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

Question

.net API 具有以下上下文构造函数：

Context (Dictionary< string, string > settings)

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

具体来说，我对如何让 Z3 产生一个 unsat 核心感兴趣，即相当于 SMT lib 产生-unsat-cores。

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