将`appendo`关系从smt2转换为python [英] Converting `appendo` relation from smt2 to python

问题描述

最近我正在学习 SMT 求解器.虽然 SMT 求解器对我来说是一个新概念，但它让我想起了逻辑编程，例如Prolog 和 minikanren.所以我在SMT求解器中尝试了一个经典的逻辑编程示例.

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.

示例是appendo 关系，我们可以向后执行它.即给定一个输出列表，返回所有可能的两个输入，当连接这两个输入列表时返回输出列表.

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.

以下是appendo关系，我在z3/smt2求解器中实现:

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.

根据这个问题，似乎不可能自动获得所有满意的模型在纯 smt2 (?) 中.我们必须使用一些 API 绑定.

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

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

I tried z3 python API for hours, but failed.

有人可以帮我将上面的 smt2 代码转换为 z3py 吗?(z3py 的文档很简短，读起来很吃力，尤其是关于如何定义递归函数，见谅...)

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 ...)

非常感谢.

以下是我未完成的代码:

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)

## ...

推荐答案

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

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.

以下是您在 Python 中编写问题的方式:

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

这就是我相信你正在寻找的.请注意使用 FreshConst 来避免您遇到的错误，并且 while 循环确保我们迭代所有可能的解决方案.

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.

请注意，虽然 z3 支持递归函数，但它相当挑剔；如果你有复杂的约束，你最终可能会得到 unknown 作为答案，或者你会得到很长的执行时间甚至无限的电子匹配循环.

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.

这篇关于将`appendo`关系从smt2转换为python的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！