問題タブ [z3-fixedpoint]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
z3 - C# で存在量指定子と固定小数点 Z3 を実行するとエラーが表示される
固定小数点で ctx.mkExist を使おうとしたのですが、「contains recursive predicate」というエラーが発生しました。理由はわかりません。固定小数点で ctx.MkExists を使用する方法?例: ラム>=0 AND inv(c,i) AND phi(c+lamb,i) => phi(c，i)
「AccessViolationException was unhandlered ,Attempted to read or write protected memory. これは多くの場合、他のメモリが破損していることを示しています。 」というエラーが発生します。ctx.MkExists() への実行時
z3 - z3を使用してFixedpointで変数の制約を取得する方法は?
d>=0.0 のような固定小数点 phi の要素の制約を取得したいのですが、Z3 でそれを実現するにはどうすればよいですか?
z3 - z3を使用してFixedpointの変数の制約を取得する方法は？
固定小数点phiの要素の制約を取得したいのですが、次の例では、制約はc2 <= c1 + 5.0、c1> = 5.0である必要があります。これは、Z3でどのように実現するかです。または、Z3で固定小数点を使用せずにそれを行う方法はありますか
z3 - Z3 の get-answer はサポートされていません
Z3 の固定小数点エンジンを使用して、いくつかのユニバーサル ホーン式をエンコードしています。クエリは unsat であることが判明しました。Z3Py では、get_answer() を使用すると、評価が解釈されていない関係に返されます。ただし、SMTLIB2 形式では、get-answer は を返しますunsupported。これが私のプログラムです：
Z3 を使用して取得している出力version 4.3.2は次のとおりです。
Z3Py では、固定小数点コンテキストを作成してfp=Fixedpoint()から実行するprint fp.get_answer()と、評価がI、I1およびに返されerrます。SMTLIB2 形式で同じものを取得する方法はありますか? ありがとう。
recursion - muZ3: 非決定的な再帰呼び出し
muZ3 リレーション仕様で非決定論的に再帰呼び出しを実行する方法はありますか? 具体的には、次のような関数を翻訳したいと思います。
muZ3 ルール形式に。
z3 - 固定小数点クエリの「不明な並べ替え」エラー
queryキーワードを使用して固定小数点クエリを実行しようとすると、「不明な並べ替え」エラーが発生します。たとえば、固定小数点チュートリアルの次の例は、Z3 のオンライン バージョンで正常に動作します。
戻り値：
コマンドラインから実行すると。Linux の github リポジトリからコンパイルされた Z3 バージョン 4.4.2 を使用します。私のコマンドラインは次のとおりです。z3 -smt2 example.smt
この機能を有効にするために設定する必要があるコンパイル フラグはありますか?