z3

    1熱

    1答えて

    z3 smt証明書がこのような簡単な式で失敗するのはなぜですか？

    私は、私の卒業論文に取り組んでいる間、Microsoftのz3 smtプロバ私の使用例では、量子を含む簡単な式（等価を持つ一次論理）の充足可能性（モデルなし）をチェックする必要があります。 Z3は、このいずれかを除いて、ミリ秒単位のカップルで、私の例のすべてを解決する良い仕事を行います forall x P(f(g(f(x)))) and not P(f(g(h(c)))) 私はrise4fu
    z3 smt 2016-09-27

    0熱

    1答えて

    Z3とνz（z3opt）：

    は、私たちはZ3またはνZが使用するAUFLIRAのようなロジックを選択することができることを知っているPythonのAPI使用して設定した論理書き込みによって（またはz3optを、最適化Z3の支店） (set-logic AUFLIRA) 入力.smt2ファイルです。 しかし、このロジックをに設定する必要がある場合は、Python APIを使用してください。どの方法でこれを行うことができます
    python z3 z3py 2016-09-28

    1熱

    1答えて

    νz（z3opt）：Java APIを使用してOptimizeオブジェクトを作成できません

    Java APIを使用してMax-SMTを使用しようとしています。以下は私の試みです： Optimize opt = ctx.mkOptimize(); opt.Add(hardConstraints); for(BoolExpr c : C){ opt.AssertSoft(c, 1, "group"); } しかし、optが作成された最初のライン、でランタイムエラーがありま
    z3 2016-10-02

    3熱

    1答えて

    （：VAR 0）Z3数量詞の体内に

    私はZ3 OCamlのAPIの数量詞の身体、その文字列である (exists ((u_1 Int)) (= u_1 x5)) はQuantifier.get_bodyによって、私は発現を得る例えば数量詞を取得すると (= (:var 0) x5) この式では、u_1の名前は新しく変わった変数に変更されているようですが、式の種類（：var 0）とそれをどのように戻すかはわかりませんそのボディ
    z3 2016-10-03

    1熱

    1答えて

    マルチコアサーバーでZ3を使用する

    Z3専用のシステムをセットアップしたいと思う。 4つのコアがあり、マシンのすべてのパワーを使いたいとしましょう。 約1000個のインクリメンタルアサートを持つ大きな数式を解くことになります。 私は数式を並列に解きたいと思っています。私はthis questionを読んでおり、数式を解くすべてのインスタンスに対してユニークなContextを作成する必要があることがわかります。 私の質問は、完全なシス
    c++ multithreading z3 multicore 2016-10-05

    2熱

    1答えて

    Z3 smtlib2式から宣言を得るには？

    C++ APIを使ってZ3を段階的に解決したいと思います。 これについていくつかの古い質問、2012年、すでにあります。私は新しいZ3バージョンと解決策があるかどうかを知りたい Z3 4.0 Z3_parse_smtlib2_string Z3 4.0: get complete model Z3 4.3.1 C-API parse_smtlib2_string: Where to get dec
    z3 2016-10-05

    0熱

    1答えて

    Z3のOCamlライブラリがセグメント化エラーをスローする

    Z3モジュールを使用してZ3ソルバとインターフェイスする次のOCamlコードスニペットを考えてみましょう。コードは、2つの整数の引数を受け入れ、単一のコンストラクタTとZ3に新しいTPairデータ型を定義しようとします： open Z3 open Z3.SMT open Z3.Expr open Z3.Sy
    ocaml z3 2016-10-06

    0熱

    1答えて

    z3py：私はZ3のPythonのAPIを使用しています具体的な値

    でネストされた店舗を簡素化し、[バージョン4.4.2 - 64ビット]と私はZ3が、この場合には式を簡素化する理由を理解しようとしています： >>> a = Array('a', IntSort(), IntSort()) >>> a = Store(a, 0, 1) >>> a = Store(a, 0, 3) >>> simplify(a) Store(a, 0, 3) それがこの
    python z3 z3py 2016-10-17

    0熱

    1答えて

    Z3py - 配列変数の制約を解く際に生成される関数k！0

    研究活動中、z3pyの配列（Python API for Z3 v4.4.2）を調べています。 なぜz3が結果としてより多くの配列関数を提供するのか疑問に思っていました。 ！Z3はKを使用していますように思え >>> A = Array('A', IntSort(), IntSort()) >>> solve(A[0] == 0) [A = [0 -> 0, else -> 0], k!0 =
    python arrays z3 z3py 2016-10-21

    1熱

    1答えて

    QF_NRAにゼロ除算が含まれていますか？

    ゼロ除算はQF_NRAに含まれていますか？ この問題では、SMT-LIB標準が混乱しています。 paper where the standard is definedでは、この点については説明しません。実際、NRAとQF_NRAはその文書のどこにも表示されません。いくつかの情報はstandard websiteで提供されています。実数は次のように定義されます。 - all terms of the
    z3 smt theorem-proving cvc4 2016-10-21
最新の質問