Is it possible to define a function with an all quantified assertion in z3 (with SMT-LIB2 interface)?

Question

My goal is to define a function, which takes an input integer sequence and outputs an integer sequence with the same length, but containing only the first element of the input sequence. For example (in pseudo-code):

f([7,5,6]) = [7,7,7]

For this I declare a function in z3 as:

(declare-fun f ((Seq Int)) (Seq Int))

and try to force the expected behavior with the assertion:

(assert 
    (forall ((arr (Seq Int)))
        (and
            (=
                (seq.len arr)
                (seq.len (f arr))
            )
            (forall ((i Int))
                (implies
                    (and
                        (>= i 0)
                        (< i (seq.len arr))
                    )
                    (=
                        (seq.at arr 0)
                        (seq.at (f arr) i)
                    )
                )
            )
        )
    ))

The problem is that the program does not terminate, which I suspect is caused by the all-quantifier. To test whether my conditions are correct I declared two constants and saw that for concrete values the conditions are correct:

(define-const first (Seq Int)
    (seq.++ (seq.unit 1) (seq.unit 2))
)
(declare-const second (Seq Int))
(assert 
    (and
        (=
            (seq.len first)
            (seq.len second)
        )
        (forall ((i Int))
            (implies
                (and
                    (>= i 0)
                    (< i (seq.len first))
                )
                (=
                    (seq.at first 0)
                    (seq.at second i)
                )
            )
        )
    )
)
(check-sat)
(get-model)

My question: How would it be possible to integrate the conditions in the assertions with the expected behavior of the f function? The function should be total, which means it should be defined for all possible input sequences, but this leads me to think that an all quantifier is definitely needed in my case.

question from:https://stackoverflow.com/questions/65906297/is-it-possible-to-define-a-function-with-an-all-quantified-assertion-in-z3-with

Answer 1

Reasoning with such recursive data-types/values is not a strong suit for SMT solvers. Most problems will require induction and SMT-solvers don't do induction out-of-the box.

Having said that, you can code what you want using the new declare-fun-rec construct:

(define-fun-rec copyHeadAux ((x (Seq Int)) (l (Seq Int))) (Seq Int)
   (ite (= 0 (seq.len l))
        (as seq.empty (Seq Int))
    (seq.++ x (copyHeadAux x (seq.extract l 1 (seq.len l))))))


(define-fun copyHead ((l (Seq Int))) (Seq Int)
   (ite (= 0 (seq.len l))
        (as seq.empty (Seq Int))
    (copyHeadAux (seq.at l 0) l)))

(define-fun test () (Seq Int) (seq.++ (seq.unit 7) (seq.unit 5) (seq.unit 6)))
(declare-const out (Seq Int))
(assert (= out (copyHead test)))
(check-sat)
(get-model)

When I run this, I get:

sat
(
  (define-fun out () (Seq Int)
    (seq.++ (seq.unit 7) (seq.unit 7) (seq.unit 7)))
  (define-fun test () (Seq Int)
    (seq.++ (seq.unit 7) (seq.unit 5) (seq.unit 6)))
  (define-fun copyHead ((x!0 (Seq Int))) (Seq Int)
    (ite (= 0 (seq.len x!0))
         (as seq.empty (Seq Int))
         (copyHeadAux (seq.at x!0 0) x!0)))
)

which is the correct answer you're looking for. But unless your constraints only involve "constant-folding" cases (i.e., where copyHead is always applied to a constant known value), you're likely to get unknown as the answer, or have the solver go into an infinite e-matching loop.

It's best to use a proper theorem prover (Isabelle, HOL, Lean, ACL2 etc.) for reasoning with these sorts of recursive definitions. Of course, SMT solvers get better over time and maybe one day they'll be able to handle more problems like this out-of-the-box, but I wouldn't hold my breath.