7

.net API には、コンテキスト用の次のコンストラクターがあります。

Context (Dictionary< string, string > settings)

可能なすべての設定のリストを取得する方法は?

具体的には、Z3 に unsat コアを生成するように依頼する方法に興味があります。つまり、SMT ライブラリの Produce-unsat-cores と同等のものです。

4

1 に答える 1

5

あなたは良い点を指摘します。.NET API に送信できるパラメーターは、.NET コードと一緒に記述されていません。ただし、彼らは C ベースの API を呼び出しており、C ベースの API のコメント ( https://github.com/Z3Prover/z3/blob/master/src/api/z3_api.h ) には構成パラメーターのセットがリストされています。コンテキストに渡すことができます。彼らです：

      - proof  (Boolean)           Enable proof generation
      - debug_ref_count (Boolean)  Enable debug support for Z3_ast reference counting 
      - trace  (Boolean)           Tracing support for VCC
      - trace_file_name (String)   Trace out file for VCC traces
      - timeout (unsigned)         default timeout (in milliseconds) used for solvers
      - well_sorted_check          type checker
      - auto_config                use heuristics to automatically select solver and configure it
      - model                      model generation for solvers, this parameter can be overwritten when creating a solver
      - model_validate             validate models produced by solvers
      - unsat_core                 unsat-core generation for solvers, this parameter can be overwritten when creating a solver
于 2013-05-16T16:44:18.007 に答える