如何獲取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上下文的所有可用配置設置的列表？

回答

相關問題