我正在使用 Microsoft 的 Z3 SMT 求解器,并且我正在尝试定义自定义类型的常量。默认情况下,这些常量似乎并不不平等。假设您有以下程序:
(declare-sort S 0)
(declare-const x S)
(declare-const y S)
(assert (= x y))
(check-sat)
这将给出“sat”,因为当然完全有可能两个相同类型的常数相等。由于我正在制作其中常数必须彼此不同的模型,这意味着我需要添加以下形式的公理
(assert (not (= x y)))
对于每对相同类型的常量。我想知道是否有某种方法可以实现这种通用,以便默认情况下每个常量都是唯一的。
您可以使用数据类型对许多编程语言中的枚举类型进行编码。在下面的示例中,排序S
具有三个要素,并且它们彼此不同。
(declare-datatypes () ((S a b c)))
这是一个完整的例子:http://rise4fun.com/Z3/ncPc http://rise4fun.com/Z3/ncPc
(declare-datatypes () ((S a b c)))
(echo "a and b are different")
(simplify (= a b))
; x must be equal to a, b or c
(declare-const x S)
; since x != a, then it must be b or c
(assert (not (= x a)))
(check-sat)
(get-model)
; in the next check-sat x must be c
(assert (not (= x b)))
(check-sat)
(get-model)
另一种可能性是使用distinct
.
(assert (distinct a b c d e))
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)