私はCの共用体のようなsmtlibで何かを実現しようとしました：
union IntBoolType
{
int i;
boolean b;
} x;
これまでの私の成果：
(declare-datatypes (Int) ((IntPart INone (part (i Int)))))
(declare-datatypes (Bool) ((BoolPart BNone (part (b Bool)))))
(declare-datatypes () ((IntBoolType (mk (ipart (IntPart Int))
(bpart (BoolPart Bool))))))
アイデアは、IntBoolTypeintまたは（xor）ブール値のいずれかを含む必要があるということです。「なし」を示すために、サブデータ型に2つのフィールドを導入しました。タイプIntBoolType（ibt1to ibt10）の定数をいくつか宣言しましたが、これらの要件をサポートするためにアサーションを定義したいと思いました。
(assert (distinct ibt1 ibt2 ibt3 ... ibt10)
(assert (xor (= (ipart ibt1) INone) (= (bpart ibt1) BNone)))
2番目のアサーションが必要です。そうしないと、INoneとで1つの解決策が得られたからBNoneです。ただし、z3は、整数値とブール値の両方を含む出力を出力するようになりました。私は何か見落としてますか？この問題をエンコードするためのよりスマートな方法はありますか？
少しバックアップして、作成した対応するMLタイプを検討してください。
type intpart = int option
type boolpart = bool option
type intbooltype = Mk of intpart * boolpart
それは常にオプションのペアです。私はあなたが望んでいたのはどちらかだと思います：
type ('a,'b) either = Left of 'a | Right of 'b
CVC4およびz3がサポートするデータ型拡張でこれを記述する方法は次のとおりです。
(declare-datatypes (U T) ((Either (Left (left U))
(Right (right T)))))
（これはCユニオンと同じではありませんが、別の話です。）
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加