CODEWITHSUNDEEP
z3
Cristian Petrescu-Prahova
Cristian Petrescu-Prahova

Reputation: 157

Compute recursive functions with Z3

I'd like to write a function to "compute" the length of a list. http://rise4fun.com/Z3/Irsl1, based on list concat in z3 and Proving inductive facts in Z3.

I can't seem to be able to make it work, it fails with a timeout. Would such a function be expressible in Z3?

The larger context is that I'm trying to model and solve questions like "how many even positive integers are less than 9?", or "there are 5 even positive integers smaller than than x, what is x?".

Upvotes: 0

Views: 519

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

The larger context is that I'm trying to model and solve questions like "how many even positive integers are less than 9?", or "there are 5 even positive integers smaller than than x, what is x?".

If this is what you are really trying to solve, then I would suggest not creating lists or comprehensions directly, but to encode problems using just arithmetic. For example, you can obtain even integers by multiplying by two, and express properties of intervals of integers using quantifiers.

For operations on sequences, there are some emerging options. For example, sequences and lengths are partially handled: http://rise4fun.com/z3/tutorial/sequences. Rather simple properties of sequences and lengths are discharged using the built-in procedure. If you start encoding properties like you hint at above, it is unlikely to do much good as the main support is around ground (quantifier-free) properties.

Upvotes: 1

Related Questions