将'appendo'关系从smt2转换为python

Question

最近我在学习SMT解决方案。虽然SMT解算器对我来说是一个新概念，但它让我想起了逻辑编程，例如Prolog和minikanren。因此，我尝试了SMT solver中逻辑编程的经典示例

这个例子是appendo关系，我们可以向后执行它。给定一个输出列表，返回所有可能的两个输入，当将这两个输入列表合并时，返回输出列表

以下是我在z3/smt2 solver中实现的appendo关系：

(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

尽管它可以工作，但这种实现的缺点是它不能自动获得所有令人满意的模型

根据this问题，在纯smt2（？）中似乎不可能自动得到所有满意的模型。我们必须使用一些API绑定

我尝试了几个小时的z3 python API，但失败了

有人能帮我把上面的smt2代码转换成z3py吗？（z3py的文档非常简短，很难阅读，特别是关于如何定义递归函数，请原谅……）

非常感谢

以下是我未完成的代码：

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

实际上，由于SMTLib语言不允许任何控制结构，所以不可能在SMTLib中获取所有模型。Python、C、Java、Haskell等的高级API更适合于此

以下是如何用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)

当我运行此程序时，我得到：

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

这就是我相信你在寻找的。请注意，使用FreshConst可以避免出现错误，并且while-循环确保我们迭代所有可能的解决方案

请注意，尽管z3支持递归函数，但它相当挑剔；如果您有复杂的约束，您可能最终得到unknown作为答案，或者您可以得到非常长的执行时间，甚至无限的e-matching循环