問題タブ [cvc4]

QF_NRA にゼロ除算は含まれますか?

SMT-LIB 標準は、この点で混乱を招きます。標準が定義されている論文では、この点について議論されていません。実際、NRA と QF_NRA はそのドキュメントのどこにも表示されていません。一部の情報は、標準 Web サイトで提供されています。実数は以下を含むものとして定義されます。

これにより、定数値に関しては分母からゼロが明示的に除外されます。ただし、後で分割は次のように定義されます。

これに続いて、次の注意事項があります。

最初の引用で(/ m 0)は は QV_NRA の数値ではないことが示されていますが、後者の引用ではそれは任意のおよびに対して充足可能/な関数であることが示されているため、これは矛盾しているように見えます。(= t1 (/ t2 0))t1t2

(/ m n)ゼロ以外の場合は実数にすぎないという記述にもかかわらず、ゼロによる除算が SMT-LIB に含まれているように見えるというのが事実上の現実nです。これは私の以前の質問に関連しています: y=1/x, x=0 は実数で満足できますか?

SMT-LIB の QF_NRA ロジックは決定可能ですか?

Tarski が、実数の多項式系が決定可能であるという意味で、非線形算術が決定可能であることを証明したことを知っています。ただし、QF_NRA には分割が含まれているため、QF_NRA がこの傘に該当するかどうかは明らかではありません。したがって、最初の問題は、QF_NRA の除算に、分母がゼロになる可能性がある変数による除算が含まれているかどうかです。 別の質問として投稿しました。これに答えるのは、それだけでは十分に難しいことが判明したためです。

ゼロによる除算が QF_NRA の一部でない場合、QF_NRA の除算は乗算に変換でき、Tarski によって証明されているように、問題は決定可能になります。除算が実際に QF_NRA に含まれている場合は、確信が持てません。私の感じでは、ゼロによる除算が発生する場合に導入された新しい変数を使用して、問題をケースごとに分割することができます。この場合、QF_NRA は依然として決定可能です。

C++ API を使用して cvc4 で bitvector を回転させようとしましたが、API は演算子式に関しては少し混乱しています。

次のコード (抜粋) を使用します。

これを実行すると、次の結果が得られます。

cvc4 の演算子構造の扱い方を知っている人はいますか?

SMT ソルバーで浮動小数点演算構造のビットブラストをどのように実装しているのか疑問に思っていました。それを行うための既存のライブラリや機能 (VHDL など) はありますか、それとも最初から実装されていますか? これは、(C ? C++ ?) コードの行数を表します。

前もって感謝します。