問題タブ [z3-fixedpoint]

z3 固定小数点ソルバーの関係へのパラメーターとして配列を使用しています。クエリを満たす証明書の配列値を取得しようとしています。これを z3 で実行すると、Uninterpreted 'a1' in A(#1,#0,#3)というエラーがスローされます。

配列が解釈されないものとして扱われるのはなぜですか? これは、解釈されていない関数を固定小数点ソルバーの関係への引数として使用できないことを意味しますか?

Python API を介して z3 の固定小数点ソルバーでバックトラックにプッシュ操作とポップ操作を使用しようとすると、「操作はエンジンでサポートされていません」という例外がソルバーによってスローされます。

プッシュ操作とポップ操作は、固定小数点ソルバーの z3py でサポートされていませんか?

Z3 と拡張 SMT-LIB2 構文を使用してホーン句を解決しています。角節の先頭は解釈されない述語であるべきだということはわかっています。しかし、次の節をどのようにホーン節の集合に書き直せばよいのだろうか。

Z3(> a 0)は、ホーン節の先頭になれないと不平を言っています。最後の節を次のように書き直すことができます。

しかし、その後、句が非常に弱くなり、 invariant の意図したモデルが得られなくなりますinv。これを行うためのより良い方法があるかどうか疑問に思います。