z3

    0

    1答えて

    私は大規模なシステムに埋め込まれたz3コードが、かなり長いタイムアウトにもかかわらず、特定の制約のセット(C++インターフェイスを通じて追加されたもの)に対する解決策を見いださないという問題があります。制約をファイルにダンプすると(ソルバーのto_smt2()メソッドを使用してcheck()の呼び出しの直前)、ファイルをスタンドアロンz3実行可能ファイルで実行すると、約4秒でシステムが解決されます

    0

    1答えて

    私は、私が変更を続け、Z3を使って増分的にチェックする必要があるAIG(およびインバーターグラフ)を持っています。私はAIGのCNF表現を生成することができ、理想的にはこれらの節を直接ソルバに供給し、コードから繰り返し呼び出すことが望ましいでしょう。 C/C++ APIを使用してZ3ソルバーに句(またはAIG)を直接追加できる方法はありますか?

    1

    1答えて

    Z3答え配列上数量を使用して、このコードが与えられたときに、「不明」: (declare-const ia Int) (declare-const ib Int) (declare-const la Int) (declare-const lb Int) (declare-const A (Array Int Int)) (declare-const a (Array Int Int))

    2

    1答えて

    .NET APIを使用して、Z3ソルバーに最小化/最大化の目的を追加する方法を探しています。何か方法はありますか?

    0

    1答えて

    私はpythonプログラムを書いていますが、その中には大きな命題式をz3インスタンスに変換する必要があります。例えば a = my_atomic_proposition("a") # Bool b = my_atomic_proposition("b", operator.ge, 42) # Real: c >= 42 c = my_atomic_proposition("c") # Bool

    0

    1答えて

    私はZ3pyの使い方が新しく、私の割り当ては両方のソリューション(satとunsat)のカウンタの例を生成することです。 unsatソリューションの反例を生成する関数はありますか?

    0

    1答えて

    私はZ3 SATソルバを使って充足可能性をチェックするブール式(形式:CNF)を持っています。私は数式が充足可能であるときに部分的な割り当てを得ることに興味があります。私はORゲートの簡単な公式でmodel.partial=trueを試しましたが、部分的な割り当てはありませんでした。 これはどのように行うことができますか?私はそれが部分的であること以外の課題には制約がありません。

    0

    1答えて

    私はドキュメントとガイドをよく見て、公正ないくつかのものを自分で試しました。しかし、私の問題に対する解決策は、私を避けています。 これは、チュートリアルでは、レコードに関して言うが、それは私のニーズに合わせ持っているか私には不明であるものです: (declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) (decla

    0

    1答えて

    と仮定X、Y、Zは整数変数であり、Aは行列であり、Iは次のように制約を表現したい: z == A[x][y] しかし、これはエラーにつながる: 例外TypeError:オブジェクトインデックスとして解釈することはできません これを行う正しい方法は何でしょうか? ======================= 具体的な例:私は最高の組み合わせスコアを持つ2つの項目を選択したい 、 ここでスコアは

    0

    3答えて

    私は、次の ウォルフラムアルファは、それが証拠を提示していないが、それは確かにtrueであることを識別することができるように思われ、最大値は(何の驚きを決定することはできませんことを証明しようとしていますそこ): declare(n, integer) $ assume(n > 0) $ is(equals(2^n - n - 1 - sum(binomial(n,k), k, 2, n),