Z3 4.0:获取完整模型 [英] Z3 4.0: get complete model
问题描述
我需要一个完整的 SMTLIB2 公式模型:
I need a complete model of an SMTLIB2 formula:
Z3(版本 3.2 和 4.0)返回所有变量的值，但不返回 var4 的值.我尝试了一些配置设置，如
Z3 (version 3.2 and 4.0) returns values for all variables but not for var4. I tried some configuration settings like
MODEL_COMPLETION = true
但它似乎不起作用.有人有建议吗?相比之下，CVC3 返回一个模型(包括 var4)，因此这不是 SMTLIB 或我的示例的问题.
but it did not seem to work. Does anybody have a suggestion? CVC3 in comparison returns a model (including var4), so it is not an issue of SMTLIB or my example.
我需要它的原因在此处详细说明.简而言之:我想使用 C API 进行增量求解.出于这个原因，我必须多次使用函数 Z3_parse_smtlib2_string.此函数需要先前声明的函数和常量作为参数.我无法通过 Z3_get_smtlib_decl 获取此信息，因为这些类型的函数仅在调用 z3_parse_smtlib_string 时起作用，而不是 Z3_parse_smtlib2_string.
The reason I need this is explained here in detail. In short: I want to use the C API for incremental solving. For this reason I have to use the function Z3_parse_smtlib2_string multiple times. This function needs previously declared functions and constants as parameters. I am unable to get this information via Z3_get_smtlib_decl because these kind of functions work just when z3_parse_smtlib_string is called, not Z3_parse_smtlib2_string.
推荐答案
您可以通过在脚本开头添加以下选项来避免此问题.
You can avoid this problem by adding the following option in the beginning of your script.
(set-option :auto-config false)
我会在下一个版本修复它.这是对正在发生的事情的简短解释.Z3 有一个 0-1 整数问题的求解器.预处理后，您的脚本被 Z3 标记为 0-1 整数问题.var4 的值在将问题视为 0-1 问题时是无关紧要"，但将问题视为整数时则不是无关紧要"问题(var4 必须是 0 或 1).默认情况下，Z3 不会显示don't care"变量的值.
I will fix it for the next release.
Here is a short explanation of what is going on.
Z3 has a solver for 0-1 integer problems. After preprocessing, your script is tagged as a 0-1 integer problem by Z3. The value of var4 is a "don't care" when the problem is viewed as a 0-1 problem, but it is not a "don't care" when the problem is viewed as an integer problem (var4 must be 0 or 1). By default, Z3 will not display the value of "don't care" variables.
MODEL_COMPLETION=true 将在您请求未包含在模型中的常量的值时完成模型.例如，如果我们执行 (eval var4)，Z3 将产生对 var4 的解释.
The MODEL_COMPLETION=true will complete the model as you request values for constants that are not included in the model. For example, if we execute (eval var4), Z3 will produce an interepretation for var4.
这篇关于Z3 4.0:获取完整模型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
