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.正解
    z3 z3py 2012-09-07

    5熱

    1答えて

    式を論理和正規形に変換するにはどうすればよいですか？

    は、式が与え言う （T1> = 2またはT2> = 3）および（T3> = 1）私はその選言標準形 を取得したい （T1> = 2及びT 3> = 1）または（t2> = 3およびt3> = 1） Z3でこれを達成する方法は？
    z3 smt 2012-07-22

    7熱

    1答えて

    Z3定量器のサポート

    単純な線形算術の問題については、定理証明器が必要です。しかし、単純な問題でもZ3を動作させることはできません。私は、それが不完全であることを承知している、しかし、この単純な例で扱うことができるようになります。 (assert (forall ((t Int)) (= t 5))) (check-sat) を、私は私が何かを見下ろすてるかどうかわからないんだけど、これは反証するのは簡単でなけれ
    z3 2012-11-02

    9熱

    1答えて

    C/C++のZ3_astツリーをトラバースする

    要するに、私はZ3_astツリーを走査し、そのノードに関連するデータにアクセスできる必要があります。それを行う方法に関するドキュメントや例は見つかりません。任意のポインタが役立つだろう。 長々として、smt2lib型の式をZ3に解析し、一定の変数を定数の代入にして、別の無関係なSMT sovlerと互換性のあるデータ構造で式を再現する必要があります。 mistralについての詳細はこの質問にとって
    z3 2012-09-19

    5熱

    1答えて

    Z3非線形算術によるパフォーマンス

    私は、非線形算術を扱うZ3の一部であると信じているところで、パフォーマンスの問題に遭遇しています。 Z3（バージョン4.1）で検証したときに完了するまでに長い時間（3分程度）がかかる簡単な具体的なBoogieの例を次に示します。 const D: int; function f(n: int) returns (int) { n * D } procedure test() returns(
    z3 2012-09-20

    6熱

    1答えて

    z3python：文字列を式に変換する

    x,y,z = Ints('x y z')とs='x + y + 2*z = 5'のような文字列を指定すると、sをz3式に簡単に変換できますか？可能であれば、変換を行うためにたくさんの文字列操作を行う必要があるようです。
    python z3 2012-09-22

    5熱

    1答えて

    現在のバージョンよりz3

    の "simplify"と "ctx-solver-simplify"の違いは何ですか？http://rise4fun.com/Z3/CqRvのように "ctx-solver-simplify"に問題があります。 http://rise4fun.com/Z3/x9X4 "ctx-solver-simplify"を "simplify"と "ctx-solver-simplify"の違いは何ですか？
    z3 2012-08-04

    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
    python z3 z3py 2012-09-26

    5熱

    1答えて

    Iは、いくつかの指定された結果/ Xペアの単純な "結果= X * T + C" は、式中、C及びTの係数を見つけたい（Z3Py）宣言関数

    ： from z3 import * x=Int('x') c=Int('c') t=Int('t') s=Solver() f = Function('f', IntSort(), IntSort()) # x*t+c = result # x, result = [(1,55), (12,34), (13,300)] s.add (f(x)==(x*t+c)) s.
    python z3 2012-08-09

    5熱

    1答えて

    TryFor in Z3は、指定された時間の後にチェックを停止しません。

    私はZ3の.NET APIを使用しています。私は呼び出すことでソルバーをインスタンス化する場合： Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit)); 及び一部のモデルのためにそれを60秒（60000ミリ秒）のTIMELIMITを与える声明 s.Check() 60秒後には戻りません。一部のモデルでは数
    .net z3 2012-08-12
最新の質問