如何获取Z3上下文的所有可用配置设置的列表？

Question

.net API具有以下Context的构造函数:

Context (Dictionary< string, string > settings)

如何获取所有可能设置的列表？

具体来说,我感兴趣的是如何让Z3生产不饱和核心,即相当于SMT lib产生的不饱和核心.

Answer 1

你说的对。可以发送到 .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