Equilvalent of array store for a record

Question

An array can store a new value and in doing so returns a new array. I know I can use the MkApp function to access the selectors of a record, how can I then replace a value of a record? I am using the .NET bindings, but as an example of the issue, here is some SMT:

(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)

Malte Schwerhoff Malte Schwerhoff · Accepted Answer · 2017-10-18T15:03:52

I don't think that there's a uniform way of updating the nth component of a record, you essentially have to "unroll" the definition of the update: when updating an array a, you basically assume that "forall j, either i is j and a[j] therefore the new value, or a[j] has the old value". Since a record has finitely many elements, you can unroll the corresponding update definition:

(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)

This isn't as concise as having a built-in update function, but OK; in particular, if your SMT code is generated by a tool.

You could also introduce an update relation (a function symbol and a quantifier would work, too, but might be problematic due to triggering):

;; 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)

Or, more generally:

;; 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)

As before, it's straight-forward to generate those update functions from the definition of a particular record.

Note: polymorphic functions aren't yet supported, you'll need a function setNth_T1_T2 per element types T1, T2 your pairs can have.

Equilvalent of array store for a record

1 Answers