如何创建包含一组其他对象的数据类型.基本上,我正在做以下代码:
(define-sort Set(T) (Array Int T))
(declare-datatypes () ((A f1 (cons (value Int) (b (Set B))))
(B f2 (cons (id Int) (a (Set A))))
))
但是Z3告诉我对A和B的未知排序.如果我删除"Set",它就像指南所说的一样.我试图使用List,但它不起作用.谁知道如何让它工作？
基本上,我想让Z3给我一个任意整数,其值大于10.所以我写下面的语句:
(declare-const x (Int))
(assert (forall ((i Int)) (> i 10)))
(check-sat)
(get-value(x))
如何将此量词应用于我的模型？我知道你可以写(assert(> x 10))来实现这一点.但我的意思是我想在我的模型量词所以每次我宣布一个整型常量,其值是保证时间将超过10所以我不必为每一个整型常量,我insert语句(主张(>×10))声明.