私は、Z3 がいくつかの紙から allsmt を実行できることに気付きました。私のプロジェクトでは、SMT 式で決定論的変数を検索する必要があります。決定論的とは、式を満足できるものにするために変数が 1 つの int 値しかとれないことを意味します。このタスクを実行できる c++/c API 関数はありますか?
これまでにできる最善の方法は、対象の各変数を否定するために、solver.check() 関数を何度も呼び出すことです。API を使用してこれを行うより高速な方法はありますか?
基本的には、allsmt と述語の抽象化/射影を行いたいと考えています。