2

这篇文章展示了如何公理化 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)))))

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

4

2 回答 2

2

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()
于 2012-06-19T15:15:11.950 回答
0

您可以为此使用排序。该len函数是在用户定义的 sort 的通用 List 上定义的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)
于 2017-11-30T12:42:02.957 回答