CODEWITHSUNDEEP
z3
pbaren
pbaren

Reputation: 111

Z3 stuck solving a seemingly simple existential

I'm using the Z3 theorem prover as a backend of a compiler to verify that function calls respect their contracts. However, Z3 appears to be stuck when confronted with solving seemingly simple existential queries.

I'm using Z3 version 4.8.5 - 64 bit (in Linux 5.0). I understand that the SMT solver is not complete for first order logic (as soon as quantifiers are involved), but still I would have expected the following to work.

This is a minimal example showing the problem, which does not terminate:

(declare-datatypes ()
  ((Term (structure (constructor Int) (arguments TermList)))
   (TermList empty (cons (head Term) (tail TermList)))))

(assert
  (forall ((A TermList) (B Term))
    (implies
      (= A (cons B empty))
      (exists ((C Term))
          (= A (cons C empty))))))

(check-sat)

Is this a well known bug or limitation of Z3?

Are there any reasonable alternatives to represent this query in such a way that Z3 can handle it?

Upvotes: 1

Views: 347

Answers (1)

alias
alias

Reputation: 30428

These sorts of problems are just not suitable for SMT solvers. There have been many queries along these lines, here're some of the most relevant ones:

Long story short, use a more powerful system to conduct such proofs, which uses SMT solvers as proof-tools under the hood. You'll have to do some manual "guiding" but the tactic language of theorem provers these days are quite well developed that they can discharge most goals of this form automatically for you. (See this paper for some Isabelle specific details: https://people.mpi-inf.mpg.de/~jblanche/frocos2011-dis-proof.pdf )

Upvotes: 1

Related Questions