数据类型包含Z3

一套我怎样才能使包含一组其他对象的数据类型。基本上，我做了下面的代码：数据类型包含Z3

(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.如果我删除“设置”它只是为导向的状态。我正在尝试使用List，但它不起作用。任何人都知道如何使它工作？

来源

2012-02-18 user1197891

您正在解决这些问题定期出现一个问题：我怎么可以混合数据类型和数组（如套，多套或者范围数据类型）？

如上Z3表示不支持在单个声明混合数据类型和数组。一种解决方案是开发用于混合数据类型+阵列理论定制解算器。 Z3包含用于开发自定义解算器的编程式 API。

开发此示例以说明编码理论与量词和触发器的功能和限制仍然有用。让我通过使用A来简化您的示例。作为解决方法，您可以定义辅助排序。解决方法并不理想，但。它说明了一些公理'黑客'。它依赖于操作语义如何在搜索过程中实例化量词。

(set-option :model true) ; We are going to display models. 
(set-option :auto-config false) 
(set-option :mbqi false) ; Model-based quantifier instantiation is too powerful here 


(declare-sort SetA)  ; Declare a custom fresh sort SetA 
(declare-datatypes() ((A f1 (cons (value Int) (a SetA))))) 

(define-sort Set (T) (Array T Bool))

然后在（Set A），SetA之间定义双射。

(declare-fun injSA ((Set A)) SetA) 
(declare-fun projSA (SetA) (Set A)) 
(assert (forall ((x SetA)) (= (injSA (projSA x)) x))) 
(assert (forall ((x (Set A))) (= (projSA (injSA x)) x)))

这几乎是数据类型声明的状态。要强制精心foundedness你可以序以A 成员关联，并强制执行组A的成员是在有理有据的排序更小：

(declare-const v Int) 
(declare-const s1 SetA) 
(declare-const a1 A) 
(declare-const sa1 (Set A)) 
(declare-const s2 SetA) 
(declare-const a2 A) 
(declare-const sa2 (Set A))

随着公理到目前为止，A1可以成员本身。

(push) 
(assert (select sa1 a1)) 
(assert (= s1 (injSA sa1))) 
(assert (= a1 (cons v s1))) 
(check-sat) 
(get-model) 
(pop)

我们现在A.

(declare-fun ord (A) Int) 
(assert (forall ((x SetA) (v Int) (a A)) 
    (=> (select (projSA x) a) 
     (> (ord (cons v x)) (ord a))))) 
(assert (forall ((x A)) (> (ord x) 0)))

通过Z3默认量词实例成员的序号关联是基于模式。上面的第一个量化断言将不会在所有的相关实例上实例化。人们可以代替断言：

(assert (forall ((x1 SetA) (x2 (Set A)) (v Int) (a A)) 
    (! (=> (and (= (projSA x1) x2) (select x2 a)) 
     (> (ord (cons v x1)) (ord a))) 
     :pattern ((select x2 a) (cons v x1)))))

公理像这样，使用两种模式（称为多模式）是相当昂贵的。他们为每对（选择x2 a）和（cons v x1）

生成实例化。从之前的成员约束现在是不可满足的。

(push) 
(assert (select sa1 a1)) 
(assert (= s1 (injSA sa1))) 
(assert (= a1 (cons v s1))) 
(check-sat) 
(pop)

但是模型不一定能够很好地形成。该集合的默认值为'true'，其中意味着该模型意味着存在会员周期，当没有一个时。

(push) 
(assert (not (= (cons v s1) a1))) 
(assert (= (projSA s1) sa1)) 
(assert (select sa1 a1)) 
(check-sat) 
(get-model) 
(pop)

我们可以通过使用下面的方法来强制执行被数据类型使用的集合是有限的接近更真实的模型。例如，每当在集合x2, 上进行会员资格检查时，我们强制执行该集合的“默认”值为'false'。

(assert (forall ((x2 (Set A)) (a A)) 
    (! (not (default x2)) 
     :pattern ((select x2 a)))))

可替换地，每当一组在一个数据类型构造发生它是有限

(assert (forall ((v Int) (x1 SetA)) 
    (! (not (default (projSA x1))) 
     :pattern ((cons v x1))))) 


(push) 
(assert (not (= (cons v s1) a1))) 
(assert (= (projSA s1) sa1)) 
(assert (select sa1 a1)) 
(check-sat) 
(get-model) 
(pop)

纵观包括额外的公理， Z3产生答案“未知”，此外模型生成的表明域SetA 是有限的（单身）。所以虽然我们可以修补默认值，但这个模型仍然不满足公理。它只满足公理模实例化。

来源

2012-02-20 00:38:27

这Z3不支持。您可以在数据类型声明中使用数组，但它们不能包含您声明的数据类型的“引用”。例如，使用即可。

来源

2012-02-18 18:27:58

数据类型包含Z3

回答

相关问题