z3

    5熱

    2答えて

    Z3は、有界データ構造に対する再帰関数の充足可能性をチェックできますか？

    私はそれがZ3 cannot check the satisfiability of formulas that contain recursive functionsを知っています。しかし、私はZ3がこのような公式を有界データ構造上で扱うことができるのだろうかと思います。たとえば、長さが最大2つのリストをmy Z3 programに定義し、関数をlastと定義してリストの最後の要素を返しました。
    z3 2011-08-16

    2熱

    1答えて

    Z3統計情報：時間は何を測定するのですか？

    -stコマンドオプションを指定してZ3 3.1を実行すると、奇妙な統計結果が表示されます。 Ctrl-Cを押すと、Z3はtotal_time <時間を報告します。そうでなければ、Z3が終了するまで待つなら、total_time> time。 「合計時間」と「時間」は何を測定するのですか？ これはバグですか（マイナーですが）（上記の違い）？ ありがとう！
    z3 2011-09-07

    2熱

    1答えて

    Z3 QBVFの質問

    前の議論をフォローアップ： (declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) (assert (forall ((y (_ BitVec 16))) (bvuge y (sx y)))) そして限りZ3に関しては (declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) (declare-fun y() (_
    z3 2011-09-09

    1熱

    1答えて

    `eval`をタイムアウトに呼び出す

    Leonardo：迅速な返信をありがとう！とても有難い。 私はZ3に次のスクリプトを養う場合：は (set-option :MBQI true) (set-option :produce-models true) (declare-fun s1 ((_ BitVec 16)) (_ BitVec 16)) (assert (forall ((s0 (_ BitVec 16))) (bvuge
    z3 2011-09-09

    3熱

    2答えて

    WindowsでScala^Z3をコンパイルする

    Win XPでScala^Z3をCygwinとJDK 1.7.0を使ってコンパイルしようとしましたが、期待通りに動作しませんでした。 私は次のようでした： - 利用SBT 0.7.4 - githubの から使用現在のScala^Z3の改正 - 利用CygwinとそのGCC - 利用JDK 1.7.0（javacの） 「SBT更新"成功しました。 \ psuter-ScalaZ3-35cb691
    scala z3 2011-09-12

    0熱

    1答えて

    Z3スコープにラベルを付けて特定のものにポップバック

    Z3スコープにラベルを付けることは可能ですか（SMTLib2構文）、特定のスコープにポップバックできますか？たとえば、次のように (push foo) ; ... (push) ; ... (pop foo) ; pops two scopes 私は(pop 2)との2つのスコープをポップすることができます知っているが、私のシナリオでは、これは私がプッシュ・ポップのペア
    scope label push pop z3 2011-08-05

    5熱

    1答えて

    Z3はCraig補間をサポートします

    Z3はCraig補間を生成できますか（少なくとも命題論理の場合は？）。 私はZ3のドキュメントでそれを見つけられませんでした。
    z3 2011-08-10

    2熱

    1答えて

    PROOF_MODEオプションが使用されていない場合は応答がありません

    私はリアルタイムタスクシステムで得られたスケジュールの堅牢性を証明するためにZ3を使用しています。このスクリプトをチェックすると、http://www.cs.ru.nl/~georgeta/script.smt2私は不満な応答を得ます。しかし、PROOF_MODE = 1オプションを使用すると、応答は飽和します。前者の場合、何が間違っている可能性がありますか？
    z3 2011-08-10

    8熱

    1答えて

    Z3を使用して部分文字列を推論できますか？

    私は部分文字列について推論するためにZ3を使用しようとしており、非直感的な振る舞いに遭遇しました。 Z3は、 'xy'が 'xy'内に現れるかどうかを尋ねられたとき 'sat'を返しますが、 'x'が 'x'であるか 'x'が 'xy'であるかを尋ねられたら 'unknown'を返します。 私は、この動作を説明するために、次のコードにコメントしました：これで問題が設定されていることを、我々はサブス
    z3 smt 2011-08-19

    3熱

    1答えて

    ビットベクトル（SMTLIB2、Z3）に値を割り当てますか？

    私はZ3バージョン3.0を使用しています。以下のように、ビットベクトル変数に値を代入したい。 しかし、Z3はエラー "無効な関数のアプリケーション、行3の位置2の引数のソートの不一致"を報告します。 私の定数＃x0aは間違っていますか？どうすればこの問題を解決できますか？ SMT-LIB 2.0標準で (set-logic QF_BV) (declare-fun a() (_ BitVec 32
    z3 2011-08-23
最新の質問