问题描述
在 SMT:检查函数的唯一性和完整性中，我给出了函数公理化并要求 Z3 提供模型.但是，由于解决带有量词的问题通常是不可判定的，因此 Z3 超时.
In SMT: check uniqueness and totality of function I gave a function axiomatization and asked Z3 for a model. However because solving something with quantifiers in it is undecidable in general, Z3 times out.
这是一个修改版本，其中int"大小写被建模为单个值:
Here is a modified version in which the "int" case is modelled as a single value:
(declare-datatypes () ((ABC int error none)))
(declare-fun f (ABC ABC) ABC)
(assert (forall ((x ABC)) (=> (or (= x int) (= x error) (= x none)) (= (f none x) none))))
(assert (forall ((x ABC)) (=> (or (= x int) (= x error) (= x none)) (= (f x none) none))))
(assert (forall ((x ABC)) (=> (or (= x int) (= x error)) (= (f error x) error))))
(assert (forall ((x ABC)) (=> (or (= x int) (= x error)) (= (f x error) error))))
(assert (forall ((x ABC) (y ABC)) (=> (and (= x int) (= y int)) (= (f x y) int))))
(check-sat)
(get-model)
因为现在的情况有限，Z3很快给出了答案:
Because there now are finitely many cases, Z3 gives an answer quickly:
sat
(model
(define-fun k!26 ((x!0 ABC)) ABC
(ite (= x!0 error) error
(ite (= x!0 int) int
none)))
(define-fun f!28 ((x!0 ABC) (x!1 ABC)) ABC
(ite (and (= x!0 error) (= x!1 int)) error
(ite (and (= x!0 int) (= x!1 error)) error
(ite (and (= x!0 error) (= x!1 error)) error
(ite (and (= x!0 int) (= x!1 int)) int
none)))))
(define-fun k!27 ((x!0 ABC)) ABC
(ite (= x!0 error) error
(ite (= x!0 int) int
none)))
(define-fun f ((x!0 ABC) (x!1 ABC)) ABC
(f!28 (k!27 x!0) (k!26 x!1)))
)
k!26 和 k!27 实际上只是返回它们的输入(通过检查所有三种情况很容易看出这一点).是否可以通过自动消除这两个函数来简化模型?
Both k!26 and k!27 actually just return their input (this is easily seen by checking all three cases). Is it possible to simplify the model by eliminating these two functions automatically?
最理想的情况是，我希望有以下内容，尽管我认为这可能是不可能的:
Optimally I would like to have something like the following, although I see that might not be possible:
(define-fun f ((x!0 ABC) (x!1 ABC)) ABC
(ite (or (= x!0 none) (= x!1 none)) none
(ite (or (= x!0 error) (= x!1 error)) error
int)))
我正在使用 Z3Py，但欢迎使用 Z3 特定和 Z3Py 特定的一般答案.
I'm using Z3Py, but both general Z3-specific and Z3Py-specific answers are welcome.
推荐答案
我不认为您可以做很多事情来指导 Z3 在这里提供更简单"的答案；因为生成的模型取决于证明的方式，即使对问题进行简单的更改也会产生不可预测的结果.特别是，您得到的模型可以随着 Z3 的下一个版本而改变.
I don't think there's much you can do to guide Z3 to provide a "simpler" answer here; as the model generated depends on how the proof was done and even simple changes to the problem can have unpredictable results. In particular, the model you get can change with the next version of Z3.
话虽如此，一个常见的技巧是在模型中eval 项.由于您当前的问题仅涉及有限域，因此您可以枚举它.如果您在脚本末尾添加以下几行:
Having said that, a common trick is to eval terms in the model. Since your current problem only involves a finite domain, you can enumerate it. If you add the following lines at the end of your script:
(eval (f int int))
(eval (f int error))
(eval (f int none))
(eval (f error int))
(eval (f error error))
(eval (f error none))
(eval (f none int))
(eval (f none error))
(eval (f none none))
然后Z3会打印:
int
error
none
error
error
none
none
none
none
也许您可以使用该输出自己构建一个更简单"的模型.当然，这只适用于域是有限的；但是您可以使用相同的技巧来评估输入域的有趣"部分，具体取决于您的问题.
Perhaps you can use that output to construct a "simpler" model yourself. Of course, this only works if the domain is finite; but you can use the same trick to evaluate "interesting" parts of the input domain, depending on your problem.
这篇关于简化模型中的函数解释的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！