Fixpoint for EC

core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala

@@ -210,6 +210,7 @@ class EquivalenceChecker(override val trees: Trees,
 
   private val models = mutable.Map.from(allModels.map(_ -> initScore))
   private val remainingCandidates = mutable.SortedSet.from(allCandidates)
+  private var nbExaminedCandidates = allCandidates.size
   private var examinationState: ExaminationState = ExaminationState.PickNext
   private val valid = mutable.Map.empty[Identifier, ValidData]
   // candidate -> list of counter-examples (can be empty, in which case the candidate is invalid but a ctex could not be extracted)
@@ -294,7 +295,14 @@ class EquivalenceChecker(override val trees: Trees,
         examinationState = ExaminationState.Examining(candId, RoundState(topN.head, topN.tail, strat, EquivLemmas.ToGenerate, 0L))
         NextExamination.NewCandidate(candId, topN.head, strat, pruned.toMap)
       case None =>
-        NextExamination.Done(pruned.toMap, getCurrentResults())
+        if (unknowns.nonEmpty && unknowns.size < nbExaminedCandidates) {
+          nbExaminedCandidates = unknowns.size
+          remainingCandidates ++= unknowns.keySet
+          unknowns.clear()
+          pickNextExamination()
+        } else {
+          NextExamination.Done(pruned.toMap, getCurrentResults())
+        }
     }
   }
 

frontends/benchmarks/equivalence/uniq2/Candidate1.scala

@@ -0,0 +1,24 @@
+import stainless.lang._
+import stainless.collection._
+
+object Candidate1 {
+  def check(element: Int, l: List[Int]): Boolean = {
+    decreases(l)
+    l match {
+      case Nil()        => { false }
+      case Cons(hd, tl) => { if (element == hd) true else check(element, tl) }
+    }
+  }
+
+  def app(l1: List[Int], l2: List[Int]): List[Int] = {
+    decreases(l1)
+    l1 match {
+      case Nil() => { l2 }
+      case Cons(hd, tl) => {
+        if (check(hd, l2)) app(tl, l2) else app(tl, l2 ++ List(hd))
+      }
+    }
+  }
+
+  def uniq(lst: List[Int]): List[Int] = { app(lst, Nil()) }
+}

frontends/benchmarks/equivalence/uniq2/Candidate2.scala

@@ -0,0 +1,35 @@
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object Candidate2 {
+  def uniq(lst: List[Int]): List[Int] = {
+    decreases(lst.size)
+    lst match {
+      case Nil() => { Nil() }
+      case Cons(hd, tl) => {
+
+        def drop(a: Int, lst_0: List[Int]): List[Int] = {
+          decreases(lst_0)
+          lst_0 match {
+            case Nil() => { Nil() }
+            case Cons(hd_0, tl_0) => {
+              if (a == hd_0) drop(a, tl_0) else hd_0 :: drop(a, tl_0)
+            }
+          }
+        }
+
+        def lem(a: Int, @induct lst: List[Int]): Unit = {
+          ()
+        } ensuring(drop(a, lst).size <= lst.size)
+
+        lem(hd, tl)
+        assert(drop(hd, tl).size <= tl.size)
+        assert(drop(hd, tl).size < lst.size)
+
+        hd :: uniq(drop(hd, tl))
+
+      }
+    }
+  }
+}

frontends/benchmarks/equivalence/uniq2/Model.scala

@@ -0,0 +1,100 @@
+import stainless.collection._
+import stainless.annotation._
+import stainless.lang._
+
+object Model {
+
+  def remove_elem_1(e: Int, lst: List[Int]): List[Int] = {
+    decreases(lst)
+    lst match {
+      case Nil() => { Nil() }
+      case Cons(hd, tl) => {
+        if (e == hd) remove_elem_1(e, tl) else hd :: remove_elem_1(e, tl)
+      }
+    }
+  }
+
+  def solution_1(lst: List[Int]): List[Int] = {
+    decreases(lst)
+    lst match {
+      case Nil()        => { Nil() }
+      case Cons(hd, tl) => { hd :: remove_elem_1(hd, solution_1(tl)) }
+    }
+  }
+
+  def drop_2(lst: List[Int], n: Int): List[Int] = {
+    decreases(lst)
+    lst match {
+      case Nil()        => { Nil() }
+      case Cons(hd, tl) => { if (hd == n) drop_2(tl, n) else hd :: drop_2(tl, n) }
+    }
+  }
+
+  def lemma_2(n: Int, @induct lst: List[Int]): Unit = {
+  } ensuring(drop_2(lst, n).size <= lst.size)
+
+  def solution_2(lst: List[Int]): List[Int] = {
+    decreases(lst.size)
+
+    def lem(n: Int, @stainless.annotation.induct lst: List[Int]): Unit = {
+      ()
+    } ensuring(drop_2(lst, n).size <= lst.size)
+
+    lst match {
+      case Nil()        => { Nil() }
+      case Cons(hd, tl) => {
+        lem(hd, tl)
+        hd :: solution_2(drop_2(tl, hd))
+      }
+    }
+  }
+
+  def is_in_3(lst: List[Int], a: Int): Boolean = {
+    decreases(lst)
+    lst match {
+      case Nil()        => { false }
+      case Cons(hd, tl) => { if (a == hd) true else is_in_3(tl, a) }
+    }
+  }
+
+  def unique_3(lst1: List[Int], lst2: List[Int]): List[Int] = {
+    decreases(lst1)
+    lst1 match {
+      case Nil() => { lst2 }
+      case Cons(hd, tl) => {
+        if (is_in_3(lst2, hd)) unique_3(tl, lst2) else unique_3(tl, lst2 ++ List[Int](hd))
+      }
+    }
+  }
+
+  def solution_3(lst: List[Int]): List[Int] = { unique_3(lst, Nil()) }
+
+  def solution_4(lst: List[Int]): List[Int] = {
+
+    def isNotIn_4(tlst: List[Int], c: Int): Boolean = {
+      decreases(tlst)
+      tlst match {
+        case Nil()        => { true }
+        case Cons(hd, tl) => { if (hd == c) false else true && isNotIn_4(tl, c) }
+      }
+    }
+
+    def uniqSave_4(l1: List[Int], l2: List[Int]): List[Int] = {
+      decreases(l1)
+      l1 match {
+        case Nil() => { l2 }
+        case Cons(hd, tl) => {
+
+          if (isNotIn_4(l2, hd)) {
+            uniqSave_4(tl, l2 ++ List(hd))
+          } else {
+            uniqSave_4(tl, l2)
+          }
+        }
+      }
+    }
+    uniqSave_4(lst, Nil())
+
+  }
+
+}

frontends/benchmarks/equivalence/uniq2/expected_outcome.json

@@ -0,0 +1,19 @@
+{
+  "equivalent": [
+    {
+      "model": "Model.solution_2",
+      "functions": [
+        "Candidate2.uniq"
+      ]
+    },
+    {
+      "model": "Model.solution_3",
+      "functions": [
+        "Candidate1.uniq"
+      ]
+    }
+  ],
+  "erroneous": [],
+  "timeout": [],
+  "wrong": []
+}

frontends/benchmarks/equivalence/uniq2/test_conf.json

@@ -0,0 +1,12 @@
+{
+  "models": [
+    "Model.solution_1",
+    "Model.solution_2",
+    "Model.solution_3",
+    "Model.solution_4"
+  ],
+  "comparefuns": [
+    "Candidate1.uniq",
+    "Candidate2.uniq"
+  ]
+}