宣言ソートまたは定義ソートによって導入されたソートを含むデータ型を定義しようとしています。ただし、次の試行はエラーになります。
(declare-sort A)
(define-sort B () Int)
(declare-datatypes ((listA (nilA) (consA (hdA A) (tlA listA))))) ;=> unknown sort 'A'
(declare-datatypes ((listB (nilB) (consB (hdB B) (tlB listB))))) ;=> unknown sort 'B'
それを行う方法はありますか？
前もって感謝します。
はい、できます。ところで、古いバージョンのZ3を使用しているようです。最新バージョンをお試しください。Z33.xはパラメトリックタイプをサポートします。そのため、データ型を宣言するための構文が少し変更されました。今、あなたは書く必要があります：
(declare-datatypes () ((listA (nilA) (consA (hdA A) (tlA listA)))))
新しい構文では、型パラメーターを指定できます。listAはパラメトリックではないため()、型パラメーターの空のリストを指定しただけです。Z3のデータ型の詳細については、Z3ガイドを参照してください。
パラメトリックタイプを使用して、次のようにエンコードすることもできlistAますlistB。
(declare-datatypes (T) ((list (nil) (cons (hd T) (tl list)))))
(define-sort listA () (list A))
(define-sort listB () (list B))