0

私はこのツリーデータ型を持っています。ここで、上下に移動できるようにしたいと考えています。しかし、実際には、ノードの親/左の子/右の子を取得できる限り、どのような構造でも機能します。

Tree = Datatype('Tree')
Tree.declare('nil')
Tree.declare('node', ('label', IntSort()), ('left', Tree), ('up', Tree), ('right', Tree))
Tree = Tree.create()

しかし、データ構造を埋める方法がわかりません...次のように一度に1ノードずつツリーを作成できると思っていましたが、それは間違った方法のようです。

trees = [Const('t' + str(i), Tree) for i in range(3)]
Tree.up(trees[0]) = Tree.nil
Tree.left(trees[0]) = trees[1]
Tree.right(trees[0]) = trees[2]
Tree.up(trees[1]) = trees[0]
Tree.up(trees[2]) = trees[0]

ご協力いただきありがとうございます。

4

1 に答える 1

2

そのようなデータ構造がどのように機能するかについて、あなたは少し間違っているように感じます。Z3 の言語、および Z3py の言語は、仮定/事実のみが存在する一次論理 (モジュロ理論) の言語です。命令型プログラミング言語との主な違いの 1 つは、破壊的な更新* がないことです。つまり、エンティティの値を更新することはできません。

あなたのコードでは、本質的にポインターを操作することによって、命令的な方法でデータ構造を構築しようとします。

Tree.up(trees[0]) = Tree.nil

おそらくあなたが念頭に置いていたのは、「trees[0].up指摘するnil」ことでした。ただし、破壊的な更新は一次言語の一部ではないため、代わりに「関数を考える」、つまり「それを想定するup(trees[0]) == nil」必要があります。このような仮定を追加するには、次のようにします ( rise4fun のオンライン)。

s = Solver()

s.add(
  Tree.up(trees[0]) == Tree.nil,
  Tree.left(trees[0]) == trees[1],
  Tree.right(trees[0]) == trees[2],
  Tree.up(trees[1]) == trees[0],
  Tree.up(trees[2]) == trees[0]
)

print s.check() # sat -> your constraints are satisfiable

破壊的な更新を行わないことの結果は、命令型プログラミング言語で一般的な方法でデータ構造を変更できないことです。trees[1].up.left != trees[1]このような更新を使用すると、たとえば割り当てtrees[1].up.left = trees[2]( ) によって、のようにツリーを変更できますtrees[1] != trees[2]。ただし、対応する仮定を追加すると

s.add(
  trees[1] != trees[2],
  Tree.left(Tree.up(trees[1])) == trees[2]
)

print s.check() # unsat

古い仮定と新しい仮定が矛盾しているため、制約がもはや満足できないことがわかります。


ちなみに、Treeデータ型の定義により、それを想定することができTree.up(nil) == someTreeます。t1 != t2が木の葉であり、 がleft(t1) == right(t1) == nilに類似していると仮定するとt2、 と の場合に矛盾が生じup(nil) == t1ますup(nil) == t2。ただし、Z3 のレベルでこれを防ぐ方法はわかりません。


* 破壊的な更新は、いわゆるパッシフィケーション変換によって仮定に変えることができるため、構文糖として追加できます。これは、たとえば、中間検証言語Boogieで行われます。

于 2013-06-11T09:28:22.830 に答える