整数の特定のシーケンスに、ある整数が少なくとも2回（たとえば8回）含まれているというアサーションを書き込もうとしています。これが私が書いたものです：
(declare-const s (Seq Int))
(assert (seq.in.re s
(re.++
re.all
(re.++
(seq.to.re (seq.unit 8))
(re.++
re.all
(re.++
(seq.to.re (seq.unit 8))
re.all))))))
実行しようとすると、次のエラーが発生します。
(error "line 11 column 11: Sort of function 're.++' does not match the declared type. Given domain: (RegEx (Seq Int)) (RegEx String) ")
だから私re.allは文字列に対してのみ定義されていると思いますか？すべての整数の正規表現を作成する方法はありますか？
SMTLib型システムはかなり弱く、re.all文字列regexpと他のシーケンスのregexpを区別できないため、見たときに混乱します。したがって、タイプエラーが発生します。
これは実際にはSMTLib標準で予想されています。http：//smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdfのセクション3.6.4を参照してください。
解決策（標準で説明されている）は、次のように、as句を使用して明示的な型を指定することです。
(define-fun allInt () (RegEx (Seq Int)) (as re.all (RegEx (Seq Int))))
(declare-const s (Seq Int))
(assert (seq.in.re s
(re.++
allInt
(re.++
(seq.to.re (seq.unit 8))
(re.++
allInt
(re.++
(seq.to.re (seq.unit 8))
allInt))))))
これは、システムが実際のタイプがどうあるべきかをコンテキストから理解することを期待する人々にとって一般的な落とし穴です。しかし、システムを単純に保つために、設計者は非常に単純な型システムを選びました。各用語は、コンテキスト情報なしで、それ自体で入力可能である必要があります。これが不可能なまれなケース（ユースケースなど）では、as入力について明示的にする手段として構文が提供されていました。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加