2

この投稿は、Z3の組み込みリストの長さ関数を公理化する方法を示しています。ただし、この関数はソート固有（ここではInt）であり、boolのリストやカスタムソートには適用できません。

; 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 スクリプトのパラメトリック公理をサポートしていません。1 つの代替方法は、プログラム 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 に答える