New annotation to issue warning if function could not be axiomatized.

src/funcheck/Annotations.scala

@@ -2,4 +2,5 @@ package funcheck
 
 object Annotations {
   class induct extends StaticAnnotation
+  class axiomatize extends StaticAnnotation
 }

src/funcheck/CodeExtraction.scala

@@ -179,6 +179,7 @@ trait CodeExtraction extends Extractors {
             for(a <- dd.symbol.annotations) {
               a.atp.safeToString match {
                 case "funcheck.Annotations.induct" => funDef.addAnnotation("induct")
+                case "funcheck.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
                 case _ => ;
               }
             }

src/purescala/FairZ3Solver.scala

@@ -202,6 +202,12 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
     if(!Settings.noForallAxioms) {
       prepareAxioms
     }
+
+    for(funDef <- program.definedFunctions) {
+      if (funDef.annotations.contains("axiomatize") && !axiomatizedFunctions(funDef)) {
+        reporter.warning("Function " + funDef.id + " was marked for axiomatization but could not be handled.")
+      }
+    }
   }
 
   private def prepareAxioms : Unit = {
@@ -228,9 +234,9 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
             val nameTypePairs = z3ArgSorts.map(s => (z3.mkFreshIntSymbol, s))
             z3.mkForAll(0, List(pattern), nameTypePairs, z3IzedEq)
           }
-          //println("I'll assert now an axiom: " + axiom)
-          //println("Case axiom:")
-          //println(axiom)
+          // println("I'll assert now an axiom: " + axiom)
+          // println("Case axiom:")
+          // println(axiom)
           z3.assertCnstr(axiom)
         }
 
@@ -392,7 +398,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
 
       reporter.info(" - Running Z3 search...")
       val (answer, model, core) : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
-        println(blockingSetAsZ3)
+        // println(blockingSetAsZ3)
         z3.checkAssumptions(blockingSetAsZ3 : _*)
       } else {
         z3SearchStopwatch.start

testcases/Test.scala

 import funcheck.Utils._
+import funcheck.Annotations._
 
 object Test {
-  sealed abstract class List
-  case class Cons(head: Int, tail: List) extends List
-  case class Nil() extends List
+    sealed abstract class List
+    case class Cons(head: Int, tail: List) extends List
+    case class Nil() extends List
 
-  def append(value: Int, list: List) : List = list match {
-    case Nil() => Cons(value, Nil())
-    case Cons(x, xs) => Cons(x, append(value, xs))
-  }
+    @axiomatize
+    def size(l: List) : Int = (l match {
+        case Nil() => 0
+        case Cons(_, t) => 1 + size(t)
+    }) ensuring(res => res >= 0)
 
-  def isSorted(list: List) : Boolean = list match {
-    case Nil() => true
-    case Cons(x, Nil()) => true
-    case Cons(x, c @ Cons(y, ys)) => x <= y && isSorted(c)
-  }
+    @axiomatize
+    def isSorted(l : List) : Boolean = l match {
+      case Nil() => true
+      case Cons(x, xs) => xs match {
+        case Nil() => true
+        case Cons(y, _) => x <= y && isSorted(xs)
+      }
+    }
 
-  def isSorted2(list: List) : Boolean = list match {
-    case Cons(x, c @ Cons(y, ys)) => x <= y && isSorted2(c)
-    case _ => true
-  }
+    def valuesWithin(l: List, lower: Int, upper: Int) : Boolean = l match {
+      case Nil() => true
+      case Cons(x, xs) => x >= lower && x <= upper && valuesWithin(xs, lower, upper)
+    }
 
-  def sameSorted(list: List) : Boolean = {
-    isSorted(list) == isSorted2(list)
-  } holds
+    def findOne(l : List) : Boolean = {
+      isSorted(l) && valuesWithin(l, 0, 3) && size(l) == 3
+    } ensuring(res => !res)
 }