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

Question

.net API 具有以下用于上下文的构造函数:

Context (Dictionary< string, string > settings)

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

具体来说，我对如何让 Z3 产生一个 unsat 核心感兴趣，即等效于 SMT lib 的 generate-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