通用列表的长度函数答案

【问题标题】：Length function for generic lists通用列表的长度函数
【发布时间】：2012-06-21 14:49:32
【问题描述】：

This post 展示了如何公理化 Z3 内置列表的长度函数。但是，该函数是特定于排序的（此处为 Int），不适用于布尔列表或自定义排序。

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

编码排序通用列表函数的最聪明的方法是什么？（如果我没记错的话，函数本身不能是泛型的）。

【问题讨论】：

标签： list function generics z3 axiom

【解决方案1】：

SMT 2.0 格式或 Z3不支持 SMT 2.0 脚本中的参数公理。一种替代方法是使用编程 API。您可以创建为给定排序创建 len 公理的函数。这是一个关于如何使用 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()

【讨论】：

看来我必须比我想象的更早地从 stdio 切换到编程 API ......谢谢！
其他：有必要用模式来保护这样的定义方程吗？正如我通常对量化公理所做的那样。此外，该指南说定义伪宏的量词由模型查找器自动检测。我认为这需要 :mbqi 为真（在我的情况下不是这样）。能否请您详细说明一下？
如果我们不提供模式，Z3 将为我们计算它们。 Len 公理不是伪宏，因为它是“递归”定义。选项 :mbqi 默认为 true。
这是否反过来意味着所有非递归定义都是伪宏？还有，伪宏对 Z3 的行为有什么影响？如果我停用 :mbqi，伪宏是否仍然受到特殊处理？
是的，所有非递归定义都被:mbqi 引擎视为宏。一个问题是:mbqi 可能没有机会运行。 Z3 仅在构建满足所有无量词约束的“候选解释”时才执行此引擎。如果您想确保在搜索开始之前展开所有定义，可以添加选项(set-option :macro-finder true)。

【解决方案2】：

您可以为此使用排序。 len 函数是在用户定义的排序T 的通用列表上定义的。只有第一个 define-sort 将 T 链接到 Int 类型。

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

【讨论】：