z3py

5熱

1答えて

previous postでは、Z3Pyをオンラインで使用してオペアンプに関するいくつかの問題を解決しました。しかし、Z3Pyのオンラインサービスが中断されたので、私はZ3 SMT-LIBオンラインを使ってこのような問題を解決しようとしています。例1：は、この問題は次のコードを使用して解決され、以下の回路にRの値を求める： (declare-const R Real) (declare-co

10熱

1答えて

Z3/PythonモデルからPython値を取得する

Z3モデルから実際のPython値を取得するにはどうすればよいですか？など。 p = Bool('p') x = Real('x') s = Solver() s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p)) s.check() print s.model()[x] print s.model()[p] プリント -1.4142

6熱

2答えて

Z3でオーバーフローを確認してください

私はZ3が初めてで、オンラインのPythonチュートリアルをチェックしていました。次に、私はBitVecsのオーバーフロー動作をチェックできると思いました。私はこのコードを書いた： x = BitVec('x', 3) y = Int('y') solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1))) および値が等しいが、x + 1が0

5熱

3答えて

z3pyチュートリアルはどこで入手できますか

rise4fun z3pyはセキュリティ上の問題のために数週間から利用できません。私はz3pyを学ぶためのいくつかのリソースを見つけようとしましたが、無駄に終わりました。 z3pyを学ぶためのいくつかのリソースをお勧めします

0熱

1答えて

Z3パワーモジュロステートメント

Z3にパワーモイド演算を実行できますか？例えば、私が並べ替えx ** y % zの式に置いている場合、Pythonにどのように関数pow(x,y,z)があるのと同様に、このタイプの式であることをZ3に伝える方法はありますか？私の前提は、（モジュラ逆数のような）オプションを解くことができるということです。

6熱

1答えて

は

は式ペルx*x - 193 * y*y = 1 z3pyでをお持ちの方程式を理解する助けが必要です： x = BitVec('x',64) y = BitVec('y',64) solve(x*x - 193 * y*y == 1, x > 0, y > 0) 結果：[y = 2744248620923429728, x = 8169167793018974721] なぜ？ P.S.正解