通用列表的长度函数 [英] Length function for generic lists

问题描述

这篇文章显示了如何为Z3的内置列表公称长度函数.但是，该函数是特定于排序的(此处为Int)，不适用于布尔值列表或自定义排序.

This post shows how to axiomatise a length function for Z3's built-in lists. However, the function is sort-specific (here Int) and not applicable to lists of bools or custom sorts.

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

编码排序通用列表函数的最聪明方法是什么?(如果我没记错的话，函数本身就不能通用).

What would be the smartest way of encoding sort-generic list functions? (If I remember correctly, functions cannot be generic per se).

推荐答案

SMT 2.0格式或Z3不支持SMT 2.0脚本中的参数公理.一种替代方法是使用编程API.您可以创建为给定排序创建 len 公理的函数.这是有关如何使用Python API进行操作的示例.

The SMT 2.0 format or Z3 do not support parametric axioms in SMT 2.0 scripts. One alternative is to use the programmatic APIs. You can create functions that create the len axiom for a given sort. Here is an example on how to do it using the 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()

这篇关于通用列表的长度函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！