Converting `appendo` relation from smt2 to python

Question

Recently I am learning SMT solver. Although SMT solver is a new concept to me, it reminds me of logic programming, e.g. Prolog and minikanren. So I tried a classic example of logic programming in SMT solver.

The example is appendo relation, which we can execute it backwards. That is given an output list, returns all possible two inputs, when concating these two input lists return the output list.

The following is the appendo relation, I implemented in z3/smt2 solver:

(define-fun-rec appendo ((l (List Int)) (s (List Int))) (List Int)
  (ite (= nil l) 
       s
       (insert (head l) (appendo (tail l) s))
     ))
     
(declare-const a (List Int))
(declare-const b (List Int))

(assert (= (appendo a b) (insert 1 (insert 2 nil))))
(check-sat)
(get-model)
(echo "solution 1:")
(eval a)
(eval b)
;; nil
;; (insert 1 (insert 2 nil))

(assert (not (= a nil)))
(assert (not (= b (insert 1 (insert 2 nil)))))
(check-sat)
(get-model)
(echo "solution 2:")
(eval a)
(eval b)
;; (insert 1 nil)
;; (insert 2 nil)

(assert (not (= a (insert 1 nil))))
(assert (not (= b (insert 2 nil))))
(check-sat)
(get-model)
(echo "solution 3:")
(eval a)
(eval b)
;; (insert 1 (insert 2 nil))
;; nil


(assert (not (= a (insert 1 (insert 2 nil)))))
(assert (not (= b nil)))

(check-sat)
;; unsat

It works though, the drawback of this implementation is that it cannot get all the satisfying models automatically.

According to this question, it seems impossible to get all the satisfying models automatically in pure smt2 (?). We must use some API binding.

I tried z3 python API for hours, but failed.

Could someone help me to convert the smt2 code above to z3py? (The z3py's docs is very brief and difficult to read, especially about how to define a recursive function, forgive me ...)

Very thanks.

The following is my uncompleted code:

from z3 import *

## Define List
def DeclareList(sort):
    List = Datatype('List_of_%s' % sort.name())
    List.declare('cons', ('car', sort), ('cdr', List))
    List.declare('nil')
    return List.create()

IntList = DeclareList(IntSort())

## Define Rec Function
appendo = RecFunction('appendo', IntList, IntList, IntList)
RecAddDefinition(appendo, [l, s], If(IntList.nil == l, s, IntList.cons(IntList.car(l), appendo(IntList.cdr(l), s)))) ## <== NameError: name 'l' is not defined

a = Const('a', IntList)
b = Const('b', IntList)

## ...

Answer 1

Indeed, getting all models in SMTLib is not really possible since SMTLib language does not allow for any control structures. High-level APIs from Python, C, Java, Haskell etc. are better suited for this.

Here's how you'd code your problem in Python:

from z3 import *

## Define List
def DeclareList(sort):
    List = Datatype('List_of_%s' % sort.name())
    List.declare('cons', ('car', sort), ('cdr', List))
    List.declare('nil')
    return List.create()

IntList = DeclareList(IntSort())

## Define Rec Function
appendo = RecFunction('appendo', IntList, IntList, IntList)
l = FreshConst(IntList)
s = FreshConst(IntList)
RecAddDefinition( appendo
                , [l, s]
                , If(IntList.nil == l,
                     s,
                     IntList.cons(IntList.car(l), appendo(IntList.cdr(l), s)))
                )

a = Const('a', IntList)
b = Const('b', IntList)

solver = Solver()
solver.add(appendo(a, b) == IntList.cons(1, IntList.cons(0, IntList.nil)))

while solver.check() == sat:
    m = solver.model()

    v_a = m.eval(a, model_completion=True)
    v_b = m.eval(b, model_completion=True)

    print("Solution:")
    print("  a = " + str(v_a))
    print("  b = " + str(v_b))

    block = Or(a != v_a, b != v_b)
    solver.add(block)

When I run this, I get:

Solution:
  a = nil
  b = cons(1, cons(0, nil))
Solution:
  a = cons(1, nil)
  b = cons(0, nil)
Solution:
  a = cons(1, cons(0, nil))
  b = nil

which is what I believe what you're looking for. Note the use of FreshConst to avoid the error you were getting, and the while-loop ensures we iterate over all possible solutions.

Note that recursive-functions, while supported by z3, are rather finicky; and if you have complicated constraints you might end up getting unknown as answer, or you can get really long execution times or even infinite e-matching loops.