私は Z3 にあまり詳しくありませんが、いくつかのプロジェクトを実行するために使用する必要があります。
私はZ3 ラケット バインディングを使用しています。これには SMT-LIB v2 のようなテキスト インターフェイスがあり、ユニバーサル量指定子を削除できますが、まだサポートされていませんがdeclare-sort、私のモデルには何らかのカスタマイズされた型定義が必要です (方法が思いつきません)。まだ私のモデルでのみ使用するIntには..)
declare-sort
この場合、バインディングを使用したい場合、モデルでの機能を取得するにはどうすればよいでしょうか? Z3にも似たようなものはありますか？
または、Z3 でサポートされていないタイプで作業するための通常のヒントは何ですか?