将 `appendo` 关系从 smt2 转换为 python
Converting `appendo` relation from smt2 to python
最近在学习SMT求解器。虽然 SMT 求解器对我来说是一个新概念,但它让我想起了逻辑编程,例如Prolog 和 minikanren。于是尝试了SMT solver中逻辑编程的经典例子
例子是appendo
关系,我们可以反向执行。给定一个输出列表,return所有可能的两个输入,当连接这两个输入列表时return输出列表。
下面是appendo
关系,我在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
虽然可行,但此实现的缺点是无法自动获得所有令人满意的模型。
根据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)
## ...
事实上,在 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
作为答案,或者你可能会得到很长的执行时间甚至无限的电子匹配循环。
最近在学习SMT求解器。虽然 SMT 求解器对我来说是一个新概念,但它让我想起了逻辑编程,例如Prolog 和 minikanren。于是尝试了SMT solver中逻辑编程的经典例子
例子是appendo
关系,我们可以反向执行。给定一个输出列表,return所有可能的两个输入,当连接这两个输入列表时return输出列表。
下面是appendo
关系,我在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
虽然可行,但此实现的缺点是无法自动获得所有令人满意的模型。
根据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)
## ...
事实上,在 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
作为答案,或者你可能会得到很长的执行时间甚至无限的电子匹配循环。