私はソルバーの関数を使って離散時間をモデル化しています。問題は今はz3.Function('f', IntSort(), IntSort())
のような関数を使用し、関数への負の入力値は時間がt = 0で始まるため実際には適用できないということです。これは、ソルバーが負の時間の解決策を見つけることが全く考慮されていないので、私が物事をprooveしたいときに問題を引き起こします。Z3にUnsignedIntSortはありますか?
私の質問は:z3には何らかの種類の符号なしint sort(UnsignedIntSort
)がありますか?
私はそのような並べ替えを認識していません。しかし、 'unsigned int '型であるべき各定数(または関数)に' 0 <= x'という制約を追加することはできませんか? –