z3 - Z3 のレコード データ型のすべての可能な値は?

Question

異なるタイプの 6 つの要素で構成される z3 でレコード データ型を定義しようとしています。これが私がやった方法です: (declare-datatypes () ((S (mk-pair (p1 (P1type)) (p2 (P2type)) (p3 (P3type)) (m1 (bool)) (m2 (bool))) (m3 (bool)) )))) しかし、(forall (x1 S)) を使用すると、ソルバーはデータ型の評価のすべての可能な組み合わせを考慮していないようです。私が何か間違ったことをしている場合はお知らせいただければ幸いです。または、z3 が S の評価のすべての組み合わせを考慮することを期待すべきではありません。どうもありがとう、Fathiyeh

Answer 1

あなたの例へのパーマリンクは次のとおりです: http://rise4fun.com/Z3/0sl11

このモデルは、関数 LS と thau の解釈を生成します。これらの関数はどちらも、値を S からブール値にマップします。したがって、それらは述語です。モデルは、式を満たすこれらの述語の可能な値を示します。各ケースを明示的にリストして述語を定式化する必要はありません。これらの述語は通常、大きな if-then-else 式として記述されます。最後の else ブランチには、if ブランチで明示的に処理されない値のデフォルト ケースが含まれています。