Infinite loop with recursive list

[Stevendeo]

Alt-ergo seems to enter an infinite loop on the following example:

type 'a t = Cons of {elt : 'a; tail : 'a t} | Nil

function length (list : 'a t) : int =
  match list with
  | Nil -> 0
  | Cons(_, l') -> length(l') + 1
end

logic l : int t

goal g: length(l) <= 4

[Halbaroth]

The dolmen frontend rejects this file: Gbury/dolmen#121

[bclement-ocp]

This is somewhat expected because the definition for length gets expanded to:

logic length : 'a t -> int

axiom length_ext : forall list : 'a t.
  length(list) =
  match list with
  | Nil -> 0
  | Cons(_, l') -> length(l') + 1
  end

and length_ext has triggers length(list) but instantiating length causes the definition to trigger again immeidately (actually in the next round I think) on the tail.

The smt2 version of that file is:

(set-logic ALL)

(declare-datatype List
  (par (A) ((cons (elt A) (tail (List A))) (nil))))

(define-fun-rec length ((l (List Int))) Int
  (ite ((_ is nil) l)
       1
       (+ (length (tail l)) 1)))

(declare-const l (List Int))
(assert (not (<= (length l) 4)))

(check-sat)

where we also loop.

Z3 has specific support for recursive functions (I have already mentioned this offline, and still think it would be worth it to explore a similar implementation) and answers sat here, but also goes into an infinite loop if we give it the "raw" definition instead:

(declare-fun length ((List Int)) Int)

(assert
(forall ((l (List Int)))
 (=
   (length l)
   (ite ((_ is nil) l)
        0
        (+ (length (tail l)) 1)))))

CVC5 terminates quickly in both cases and answers unknown, but I am not entirely sure by what logic exactly. One thing that comes to mind is we can notice that a "ground" model has been found, i.e. a model for which we have length(x) > 4 and the quantified axioms are true for all the ground terms in the model (but that has its own issues).

In any case, we need some feedback from model generation somehow to stop us from expanding the definition infinitely. Another thing we could investigate is to wait until we have learnt (either through propagation or through a sat-solver decision) that we are exploring the "then" branch before triggering the next instantiation -- I don't know if we do that currently.

[Halbaroth]

After #1087, the infinite loop disappeared but the current implementation of #1093 produces a wrong model. I'll investigate what's happened.