1

C API と smtlib2 を介して Z3 をインクリメンタル ソリューションに使用しようとしています。残念ながら、いくつかの単純な式をアサートし、それをチェックし、そのモデルを取得し、何か追加をアサートしてから再度チェックすると、セグメンテーション違反が発生しました。これは、何か新しいことをアサートしなくても発生します。つまり、モデルをチェックして取得し、再度チェックするときに発生します。エラーを再現するための最小限の例を次に示します。

#include<z3.h>

int main()
{
  Z3_config cfg = Z3_mk_config();
  Z3_context ctx = Z3_mk_context(cfg);
  Z3_ast fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () Int) (assert (= a 0))", 0, 0, 0, 0, 0, 0);
  Z3_solver solver = Z3_mk_solver(ctx);
  Z3_solver_assert(ctx, solver, fs);
  Z3_solver_check(ctx, solver);
  Z3_model m = Z3_solver_get_model(ctx, solver);
  Z3_solver_check(ctx, solver);
  Z3_del_config(cfg);
  return 0;
}

2 つの Z3 バージョン (Mac 64 ビットでは 4.3.1、Ubuntu 64 ビットでは 4.1) を試しました。

ヘルプ、ヒント、または回避策をいただければ幸いです。API を間違った方法で使用している可能性があります。

どうもありがとう、

エリザベス

4

1 に答える 1

1

参照カウントを使用したコードのバージョンを次に示します。参照カウントを削除するとクラッシュします。

void main() {
    Z3_config cfg = Z3_mk_config();
    Z3_context ctx = Z3_mk_context(cfg);
    Z3_ast fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () Int) (assert (= a 0))", 0, 0, 0, 0, 0, 0);
    Z3_inc_ref(ctx, fs);
    Z3_solver solver = Z3_mk_solver(ctx);
    Z3_solver_inc_ref(ctx, solver);
    Z3_solver_assert(ctx, solver, fs);
    Z3_solver_check(ctx, solver);
    Z3_model m = Z3_solver_get_model(ctx, solver);
    Z3_model_inc_ref(ctx, m);
    Z3_solver_check(ctx, solver);


    // work with model

    Z3_solver_dec_ref(ctx, solver);
    Z3_model_dec_ref(ctx, m);
    Z3_dec_ref(ctx, fs);
    Z3_del_config(cfg);
 }

ところで。C++ API は、すべての参照カウントの詳細を非表示にします。作業がはるかに便利です。

于 2013-04-09T20:03:53.273 に答える