SMT入力用にcvc4のユーザ定義シンボルのオーバーロードを有効にするオプションはありますか？

Question

1.2からSMT-LIB言語のバージョンでは、ユーザー定義シンボルのオーバーロードが許可されていました。標準のバージョン2.0以降、オーバーロードは理論のシンボルに制限されています。

しかし、SMTソルバーの中には、ユーザー定義のシンボルが過負荷になることがあります。私の使用例では便利です。証拠の義務は、過負荷で自動的に生成されます。 cvc4をSMTソルバーの私のポートフォリオに追加しましたが、オーバーロードされたユーザーシンボルの解析エラーが発生することがわかりました。

これはSMT-LIB標準に準拠する正しい方法ですが、私は次のことを知りたいと思います：CVC4にこのようなチェックを無効にするオプションがあります。オーバーロードされたユーザーシンボルの曖昧さを解消する

Answer 1

残念ながら、CVC4には、過負荷のユーザーシンボルをサポートするオプションはありません。各ユーザーシンボルは一意でなければなりません。