Equalvalent数组存储记录

一个数组可以存储一个新的值，并在这样做返回一个新的数组。我知道我可以使用MkApp函数来访问记录的选择器，然后如何替换记录的值？我使用的是.NET绑定，但随着问题的例子，这里是一些SMT：Equalvalent数组存储记录

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) 
(declare-const p1 (Pair Int Int)) 
(declare-const p2 (Pair Int Int)) 
(assert (= p1 p2)) 
(assert (> (second p1) 20)) 
;How to replace (second p1) with 0 
(check-sat) 
(get-model)

来源

2017-10-18 R4D4

我不认为有更新记录的ñ个分量的统一方式，你基本上必须“展开”更新的定义：当更新数组a时，你基本上假设“所有的j，无论i是j还是a [j]因此是新值，或者[j]旧值“。由于创纪录的有穷个元素，可以展开相应的更新定义：

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) 

(declare-const p1 (Pair Int Int)) 
(assert (= (first p1) 1)) 
(assert (= (second p1) 2)) ;; p1 is (1, 2) 

(declare-const p2 (Pair Int Int)) 
(assert 
    (and 
    (= (first p2) (first p1)) 
    (= (second p2) 0))) 

(check-sat) 
(get-model) ;; p2 could be (1, 0)

这不是为具有内置更新功能简洁，但确定;特别是如果您的SMT代码是由工具生成的。

你也可以引入更新的关系（函数符号和量词会的工作，太多，但可能会出现问题，由于触发）：

;; Read: "updating p1's second element to v yields p2" 
(define-fun setSecond ((p1 (Pair Int Int)) (v Int) (p2 (Pair Int Int))) Bool ;; analogous for setFirst 
    (and 
    (= (first p2) (first p1)) 
    (= (second p2) v))) 

(declare-const p3 (Pair Int Int)) 
(assert (setSecond p2 77 p3)) 

(check-sat) 
(get-model) ;; p3 is (1, 77)

，或者更一般地说：

;; Read: "updating p1's ith element to v yields p2" 
(define-fun setNth ((p1 (Pair Int Int)) (i Int) (v Int) (p2 (Pair Int Int))) Bool 
    (and 
    (= (first p2) (ite (= i 1) v (first p1))) 
    (= (second p2) (ite (= i 2) v (second p1))))) 

(declare-const p4 (Pair Int Int)) 
(assert (setNth p3 1 -77 p4)) 

(check-sat) 
(get-model) ;; p4 is (-77, 77)

和以前一样，直接从特定记录的定义中生成更新函数。

注意：多态函数尚未支持，您需要一个函数setNth_T1_T2每个元素类型T1，T2您的配对可以拥有。

来源

2017-10-18 15:03:52

Equalvalent数组存储记录

回答

相关问题