Merge branch 'master' of laragit.epfl.ch:projects/leon-2.0

README

+This is Leon 0.2.0
+
+To build it, you will need, for example, the following:
+  * Java Runtime Environment, from Oracle, e.g. Version 7 Update 5 
+    (to run xsbt and scala)
+  * Scala, from Typesafe, e.g. version 2.9.1
+  * xsbt, e.g. version 0.11.3: download sbt-launch.jar, run it with java -jar
+    (to built Leon)
+  * a recent GLIBC3 or later, works with e.g. apt-get
+    (for Z3)
+  * GNU Multiprecision library, e.g. gmp3, works with e.g. apt-get
+    (for Z3)
+
+To build, type this:
+
+xsbt clean   
+xsbt package # takes a while
+xsbt script
+
+Then you can try e.g.
+
+./run-demo demo/RedBlackTree.scala
+
+and get something like this:
+
+[ Info  ] . ┌─────────┐
+          ╔═╡ Summary ╞═══════════════════════════════════════════════════════════════════════╗
+          ║ └─────────┘                                                                       ║
+          ║ add                       postcond.           valid               Z3-f+t    0.314 ║
+          ║ add                       precond.    (82,14) valid               Z3-f+t    0.020 ║
+          ║ add                       precond.    (82,18) valid               Z3-f+t    0.005 ║
+          ║ balance                   postcond.           valid               Z3-f+t    0.409 ║
+          ║ balance                   match.      (91,19) valid               Z3-f+t    0.034 ║
+          ║ blackHeight               match.      (51,39) valid               Z3-f+t    0.004 ║
+          ║ buggyAdd                  postcond.           invalid             Z3-f+t    4.084 ║
+          ║ buggyAdd                  precond.     (87,8) invalid             Z3-f+t    0.111 ║
+          ║ buggyBalance              postcond.           invalid             Z3-f+t    0.055 ║
+          ║ buggyBalance              match.     (105,19) invalid             Z3-f+t    0.007 ║
+          ║ ins                       postcond.           valid               Z3-f+t    6.577 ║
+          ║ ins                       precond.    (63,40) valid               Z3-f+t    0.021 ║
+          ║ ins                       precond.    (65,43) valid               Z3-f+t    0.005 ║
+          ║ makeBlack                 postcond.           valid               Z3-f+t    0.007 ║
+          ║ redNodesHaveBlackChildren match.      (35,56) valid               Z3-f+t    0.003 ║
+          ║ size                      postcond.           valid               Z3-f+t    0.012 ║
+          ╚═══════════════════════════════════════════════════════════════════════════════════╝
+
+Additional information:
+=======================
+Sample output of 
+  ldd lib-bin/lib3.so
+is:
+	linux-gate.so.1 =>  (0x00b13000)
+	libgmp.so.3 => /usr/lib/libgmp.so.3 (0x00110000)
+	libstdc++.so.6 => /usr/lib/i386-linux-gnu/libstdc++.so.6 (0x0016f000)
+	libm.so.6 => /lib/i386-linux-gnu/libm.so.6 (0x0025a000)
+	libgcc_s.so.1 => /lib/i386-linux-gnu/libgcc_s.so.1 (0x00709000)
+	libc.so.6 => /lib/i386-linux-gnu/libc.so.6 (0x004d9000)
+	/lib/ld-linux.so.2 (0x002ab000)

testcases/Sat.scala

@@ -172,27 +172,6 @@ object Sat {
     case Not(Var(n)) => ClauseCons(VarCons(-n, VarNil()), ClauseNil())
     case Var(n) => ClauseCons(VarCons(n, VarNil()), ClauseNil())
   }
-  def property1(formula: Formula, trueVars: Set[Int]): Boolean = {
-    val dnfFormula = dnfNaive(formula)
-    eval(formula, trueVars) == evalDnf(dnfFormula, trueVars)
-  } holds
-
-  def property2(formula: Formula, trueVars: Set[Int]): Boolean = {
-    val cnfFormula = cnfNaive(formula)
-    eval(formula, trueVars) == evalCnf(cnfFormula, trueVars)
-  } holds
-
-  def propertyWrong1(formula: Formula, trueVars: Set[Int]): Boolean = {
-    val dnfFormula = dnfNaive(formula)
-    isSatDnf(dnfFormula)
-  } holds
-
-  def property3(formula: Formula, trueVars: Set[Int]): Boolean = {
-    val dnfFormula = dnfNaive(formula)
-    if(!isSatDnf(dnfFormula)) eval(formula, trueVars) else true
-  } holds
-
-
 
   def vars(formula: Formula): Set[Int] = formula match {
     case Var(n) => Set(n)
@@ -211,6 +190,23 @@ object Sat {
     case ClauseLit(b) => b
   }
 
+  def simplify(formula: ClauseList): ClauseList = formula match {
+    case ClauseNil() => ClauseNil()
+    case ClauseCons(cl, cls) => simplify(cl) match {
+      case VarNil() => ClauseLit(false)
+      case VarLit(b) => if(!b) ClauseLit(false) else ClauseCons(VarLit(b), simplify(cls))
+      case vs => ClauseCons(vs, simplify(cls))
+    }
+    case ClauseLit(b) => ClauseLit(b)
+  }
+
+  def simplify(vars: VarList): VarList = vars match {
+    case VarNil() => VarNil()
+    case VarLit(b) => VarLit(b)
+    case VarCons(VarLit(b), vs) => if(b) VarList(true) else simplify(vs)
+    case VarCons(v, vs) => VarCons(v, simplify(vs))
+  }
+
   //for substitute we assume we are dealing with a cnf formula
   def substitute(formula: ClauseList, variable: Int, value: Boolean): ClauseList = formula match {
     case ClauseNil() => ClauseNil()
@@ -223,8 +219,8 @@ object Sat {
     case VarLit(b) => VarLit(b)
     case VarCons(v, vs) => 
       if     (v == variable && value)   VarLit(true)
-      else if(v == variable && !value)  substitute(vs, variable, value)
-      else if(v == -variable && value)  substitute(vs, variable, value)
+      else if(v == variable && !value)  VarCons(VarLit(false), substitute(vs, variable, value))
+      else if(v == -variable && value)  VarCons(VarLit(false), substitute(vs, variable, value))
       else if(v == -variable && !value) VarLit(true)
       else                              VarCons(v, substitute(vs, variable, value))
   }
@@ -244,14 +240,41 @@ object Sat {
     case ClauseLit(b) => b
     case _ => {
       val chosenVar = choose(formula)
-      val lhs = dpll(substitute(formula, chosenVar, true))
-      val rhs = dpll(substitute(formula, chosenVar, false))
+      val lhs = dpll(simplify(substitute(formula, chosenVar, true)))
+      val rhs = dpll(simplify(substitute(formula, chosenVar, false)))
       lhs || rhs
     }
   }
 
 
 
+  def property1(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val dnfFormula = dnfNaive(formula)
+    eval(formula, trueVars) == evalDnf(dnfFormula, trueVars)
+  } holds
+
+  def property2(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val cnfFormula = cnfNaive(formula)
+    eval(formula, trueVars) == evalCnf(cnfFormula, trueVars)
+  } holds
+
+  def propertyWrong1(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val dnfFormula = dnfNaive(formula)
+    isSatDnf(dnfFormula)
+  } holds
+
+  def property3(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val dnfFormula = dnfNaive(formula)
+    if(!isSatDnf(dnfFormula)) eval(formula, trueVars) else true
+  } holds
+
+  def property4(formula: Formula): Boolean = {
+    val cnfFormula = cnfNaive(formula)
+    val dnfFormula = dnfNaive(formula)
+    isSatDnf(dnfFormula) == dpll(cnfFormula)
+  }
+
+
 //  def main(args: Array[String]) {
 //    val f1 = And(Var(1), Or(Var(1), Not(Var(2)), Var(3)), Var(2), Not(Var(3)))
 //    val dnff1 = clauses2list(dnfNaive(f1))

testcases/master-thesis-regis/ArrayBubbleSort.scala

+import leon.Utils._
+
+object ArrayBubbleSort {
+  def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+    require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
+    if (l==u) true else a(l) <= a(l+1) && sorted(a,l+1,u)
+  }
+
+  /* The calculus of Computation textbook */
+  def bubbleSort(a: Array[Int]): Array[Int] = ({
+    require(a.length >= 1)
+    var i = a.length - 1
+    var j = 0
+    val sa = a.clone
+    (while(i > 0) {
+      j = 0
+      (while(j < i) {
+        if(sa(j) > sa(j+1)) {
+          val tmp = sa(j)
+          sa(j) = sa(j+1)
+          sa(j+1) = tmp
+        }
+        j = j + 1
+      }) invariant(
+            j >= 0 &&
+            j <= i &&
+            i < sa.length &&
+            sa.length >= 0 &&
+            partitioned(sa, 0, i, i+1, sa.length-1) &&
+            sorted(sa, i, sa.length-1) &&
+            partitioned(sa, 0, j-1, j, j)
+          )
+      i = i - 1
+    }) invariant(
+          i >= 0 &&
+          i < sa.length &&
+          sa.length >= 0 &&
+          partitioned(sa, 0, i, i+1, sa.length-1) &&
+          sorted(sa, i, sa.length-1) 
+          && sa.length == a.length // necessary
+       )
+    sa
+  }) ensuring(res => sorted(res, 0, a.length-1))
+
+  def partitioned(a: Array[Int], l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+    require(a.length >= 0 && l1 >= 0 && u1 < l2 && u2 < a.length)
+    if(l2 > u2 || l1 > u1)
+      true
+    else {
+      var i = l1
+      var j = l2
+      var isPartitionned = true
+      (while(i <= u1) {
+        j = l2
+        (while(j <= u2) {
+          if(a(i) > a(j))
+            isPartitionned = false
+          j = j + 1
+        }) invariant(j >= l2 && i <= u1)
+        i = i + 1
+      }) invariant(i >= l1)
+      isPartitionned
+    }
+  }
+
+/* // This also work as the definition of sorted and partitioned, and verifies:
+
+  def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+    require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
+    var k = l
+    var isSorted = true
+    (while(k < u) {
+      if(a(k) > a(k+1))
+        isSorted = false
+      k = k + 1
+    }) invariant(k <= u && k >= l)
+    isSorted
+  }
+
+*/
+}