How I can to check if a Const is containing in a List in Z3Py?

In Z3Py, I need to check if a Const type is containing in a List, I define the Datatype List and the Const, I tried to use the method Contain (https://z3prover.github.io/api/html/namespacez3py.html#ada058544efbae7608acaef3233aa4422) but it only is available for string datatype and I need for all.

def funList(sort):
    List = Datatype('List')
    #insert: (Int, List) -> List
    List.declare('insert', ('head', sort), ('tail', List)) 
    List.declare('nil')
    return List.create() 

IntList = funList(IntSort())
l1 = Const('l1', IntList)

I tried to do a loop in Z3 but it doesn't work :S

Solution

Your question isn't quite clear. Are you trying to code up some sort of list membership? (Like finding an element in a list.)

If this is your goal, I'd recommend against using a Datatype based coding. Because any function you'll write on that (like elem, length, etc.) will have to be recursive. And SMT solvers don't do well with recursive definitions of that form; as it puts the logic into the undecidable fragment. Furthermore, debugging and coding is rather difficult when recursive types like these are present as the tool support isn't that great.

If your goal is to use list-like structures, I'd recommend using the built-in sequence logic instead. Here's an example:

from z3 import *

s = Solver()

# declare a sequence of integers
iseq = Const('iseq', SeqSort(IntSort()))

# assert 3 is somewhere in this sequence
s.add(Contains(iseq, Unit(IntVal(3))))

# assert the sequence has at least 5 elements
s.add(Length(iseq) >= 5)

# get a model and print it:
if s.check() == sat:
    print s.model()

When I run this, I get:

$ python a.py
[iseq = Concat(Unit(9),
               Concat(Unit(10),
                      Concat(Unit(3),
                             Concat(Unit(16), Unit(17)))))]

This is a bit hard to read perhaps, but it's essentially saying iseq is a sequence that is concatenation (Concat) of a bunch of singletons (Unit). In more convenient notation, this would be:

iseq = [9, 10, 3, 16, 17]

And as you can see it has 5 elements and 3 is indeed this sequence as required by our constraints.

Z3's sequence logic is pretty rich, and it contains many functions that you'd want to perform. See here: https://z3prover.github.io/api/html/z3py_8py_source.html#l09944