z3: enumeration types, ADTs and recursive functions

Question

I'm trying to use z3 to solve some constraint system.

The intuition or the general encoding of the problem is done with three enumeration types Variable, Field and Class, as well as an ADT Path consisting either of a Variable or a Path extended with a Field. (gramatically x or p.f). There is also a (recursive) function substitute that substitutes a variable in a path with another path. There are two properties path-equivalence and instance-of (inductively) defined via all-quantified assertions.

A more concrete example is the following for Natural Numbers:

The classes are Zero, Succ and Nat, we have one variable a and a field p. We know that if a path is an instance of class Zero, then the path also is an instance of class Nat as well as if a path is an instance of class Succ and the path has a field p of class Nat, then the path also is an instance of class Nat.

What we are asking the solver is: Is it possible that a is a Succ and a.p is a Zero and a is not a Nat. With the expected result that it is not (unsat), as that would violate the two rules mentioned above.

(declare-datatype Variable (a))
(declare-datatype Field (p))
(declare-datatype Class (Zero Nat Succ))
(declare-datatype Path ((path-base (path-id Variable)) (path-ext (path-object Path) (path-field Field))))
(declare-fun path-equivalence (Path Path) Bool)
(declare-fun instance-of (Path Class) Bool)
(define-fun-rec substitute ((p1 Path) (x1 Variable) (p2 Path)) Path
  (ite (is-path-base p1)
    (ite (= x1 (path-id p1)) p2 p1)
    (path-ext (substitute (path-object p1) x1 p2) (path-field p1))))
(assert (instance-of (path-base a) Succ))
(assert (instance-of (path-ext (path-base a) p) Zero))
(assert (not (instance-of (path-base a) Nat)))
(assert (forall ((p3 Path)) (path-equivalence p3 p3)))
(assert (forall ((p5 Path) (p6 Path) (x2 Variable) (p7 Path) (p8 Path))
  (=> (and (path-equivalence p8 p7) (path-equivalence (substitute p5 x2 p7) (substitute p6 x2 p7)))
      (path-equivalence (substitute p5 x2 p8) (substitute p6 x2 p8)))))
(assert (forall ((p9 Path) (cls2 Class) (x3 Variable) (p10 Path) (p11 Path))
  (=> (and (path-equivalence p11 p10) (instance-of (substitute p9 x3 p10) cls2))
  (instance-of (substitute p9 x3 p11) cls2))))
(assert (forall ((p15 Path)) (=> (instance-of p15 Zero) (instance-of p15 Nat))))
(assert (forall ((p16 Path))
  (=> (and (instance-of p16 Succ) (instance-of (path-ext p16 p) Nat)) (instance-of p16 Nat))))
(check-sat)

So far so good, the solver seems to be able to refute queries that contradict the asserted axioms. The problem seem to start when we try to solve queries that have no such rule violation. E.g. Is it possible that a is a Succ and a.p is a Zero and a is not a Zero.

(declare-datatype Variable (a))
(declare-datatype Field (p))
(declare-datatype Class (Zero Nat Succ))
(declare-datatype Path ((path-base (path-id Variable)) (path-ext (path-object Path) (path-field Field))))
(declare-fun path-equivalence (Path Path) Bool)
(declare-fun instance-of (Path Class) Bool)
(define-fun-rec substitute ((p1 Path) (x1 Variable) (p2 Path)) Path
  (ite (is-path-base p1)
    (ite (= x1 (path-id p1)) p2 p1)
    (path-ext (substitute (path-object p1) x1 p2) (path-field p1))))
(assert (not (=> (and (instance-of (path-base a) Succ) (instance-of (path-ext (path-base a) p) Zero))
                 (instance-of (path-base a) Zero))))
(assert (forall ((p3 Path)) (path-equivalence p3 p3)))
(assert (forall ((p5 Path) (p6 Path) (x2 Variable) (p7 Path) (p8 Path))
  (=> (and (path-equivalence p8 p7) (path-equivalence (substitute p5 x2 p7) (substitute p6 x2 p7)))
      (path-equivalence (substitute p5 x2 p8) (substitute p6 x2 p8)))))
(assert (forall ((p9 Path) (cls2 Class) (x3 Variable) (p10 Path) (p11 Path))
  (=> (and (path-equivalence p11 p10) (instance-of (substitute p9 x3 p10) cls2))
  (instance-of (substitute p9 x3 p11) cls2))))
(assert (forall ((p15 Path)) (=> (instance-of p15 Zero) (instance-of p15 Nat))))
(assert (forall ((p16 Path))
  (=> (and (instance-of p16 Succ) (instance-of (path-ext p16 p) Nat)) (instance-of p16 Nat))))
(check-sat)

The expected result would be sat, but the solver basically "runs forever" (I terminated the call after roughly 30 mins).

Why is that the case? I suspect that it may be related to the recursive substitution function and the ADT (infinite domain) or with the axiomatic definitions of the two properties.

What would be possible directions to solve this behavior? E.g. is there an approach to translate the for the solver problematic constructs into something more suitable (Or something completely different)?

Answer 1

Quantifiers are hard for SMT solvers. Recursive definitions are hard for SMT solvers. Your problem combines both, and it's no wonder that z3 is having hard time.

Always keep in mind that SMT solvers do not do induction. And proof for any interesting property about recursive definitions will need induction. Imagine how you'd prove the property you wanted by hand. Would you use induction? If so, you're already stuck; z3 won't help you.

There are countless queries on stack-overflow regarding use of quantifiers and induction proofs using z3; here's a good answer by Leonardo to read through: Quantifier Vs Non-Quantifier

What can you do? Not much, if you want out-of-the-box SMT solution here. Perhaps you can use patterns (https://rise4fun.com/z3/tutorialcontent/guide#h28), which are tricky to use at the least and I don't see a direct application here.

However, at first glance, it seems your problem might better be addressed by the horn-solver: https://rise4fun.com/z3/tutorialcontent/fixedpoints See if you can adopt the techniques in there to apply to your problem. If not, I'd recommend using an actual theorem prover (like Isabelle, HOL, ACL2 etc.) almost all of which provide SMT tactics to help you out.

Long story short; quantifiers and recursive definitions are hard for SMT solvers to deal with. Any property that requires induction will fail to prove out-of-the-box. If you're lucky you'll get a counter-example if one exists; and most commonly you'll get a looping behavior in the e-matching engine.

Side note Incidentally, you can run z3 with increased verbosity to see what it's doing. Try z3 -v:3 If you do that on your program, you'll see that it keeps on expanding the recursive definitions, which will never prove a theorem; but might find a counter-example if there's one at the depth it's exploring. It's not the easiest output to read, but can give you an idea how the recursive-function solver works in practice. (Essentially by unrolling on demand.)