Length function for generic lists

Question

This post shows how to axiomatise a length function for Z3's built-in lists. However, the function is sort-specific (here Int) and not applicable to lists of bools or custom sorts.

; declare len as an uninterpreted function
(declare-fun len ((List Int)) Int)

; assert defining equations for len as an axiom
(assert (forall ((xs (List Int)))
  (ite (= nil xs)
    (= 0 (len xs))
    (= (+ 1 (len (tail xs))) (len xs)))))

What would be the smartest way of encoding sort-generic list functions? (If I remember correctly, functions cannot be generic per se).

Answer 1

The SMT 2.0 format or Z3 do not support parametric axioms in SMT 2.0 scripts. One alternative is to use the programmatic APIs. You can create functions that create the len axiom for a given sort. Here is an example on how to do it using the Python API.

http://rise4fun.com/Z3Py/vNa

from z3 import *
def MkList(sort):
    List = Datatype('List')
    List.declare('insert', ('head', sort), ('tail', List))
    List.declare('nil')
    return List.create()


def MkLen(sort):
    List = MkList(sort)
    Len  = Function('len', List, IntSort())
    x    = Const('x', List)
    Ax   = ForAll(x, If(x == List.nil, Len(x) == 0, Len(x) == 1 + Len(List.tail(x))))
    return (Len, [Ax])

IntList = MkList(IntSort())
IntLen,  IntLenAxioms = MkLen(IntSort())
print IntLenAxioms
s = Solver()
l1 = Const('l1', IntList)
s.add(IntLenAxioms)
s.add(IntLen(l1) == 0)
s.add(l1 == IntList.insert(10, IntList.nil))
print s.check()

Answer 2

You could use a sort for that. The len function is defined over a generic List of a user-defined sort T. Only the first define-sort links T to an Int type.

(define-sort T () Int)
(define-sort MyList() (List T))

(declare-const listlen Int)
(declare-const a MyList)
(declare-const b MyList)
(declare-const c MyList)
(declare-const d MyList)
(declare-const e MyList)

(define-fun-rec len((l MyList)) Int
    (ite
        (= l nil)
        0
        (+ (len (tail l)) 1)
    )
)
(assert (= a nil))
(assert (= b (insert 2 a)))
(assert (= c (insert 8 b)))
(assert (= d (insert 6 c)))
(assert (= e (insert 10 d)))

(assert (= listlen (len e)))

(check-sat)
(get-model)