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

在.NET API有一个背景下面的构造：如何获取Z3上下文的所有可用配置设置的列表？

Context (Dictionary< string, string > settings)

如何得到所有可能的设置列表？

具体而言，我感兴趣的是如何让Z3产生一个不饱和核心，即相当于SMT lib产生的不饱和核心。

来源

2013-05-14 S.N.

你说得很好。您可以发送到.NET API的参数不会与.NET代码一起描述。但是，他们正在调用基于C的API，并且基于C的API的注释（http://z3.codeplex.com/SourceControl/latest#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-16 16:44:18

感谢您指出这一点，也感谢尼古拉斯快速回答。我现在已经将这些信息添加到.NET和Java APIs/Docs中。 – 2013-05-17 12:42:25

@Christoph你能告诉我你在哪里添加了这个选项的文档吗？我在http://research.microsoft.com/en-us/um/redmond/projects/z3/class_microsoft_1_1_z3_1_1_context.html#ae996a436d55a3e34afe5971705ff9699上看不到它们。 – 2013-05-30 02:18:52

另外，如果我尝试'（“UNSAT_CORE”，“true”）'作为字典选项，我会得到'错误设置UNSAT_CORE，未知选项。 'una_core'也不被识别。请您告诉我选项名称是从.NET API – 2013-05-30 02:21:40

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

回答

相关问题