What is the difference in heap configurations? Separation logic with CVC5 SMT solver

Question

I am figuring out separation logic and trying to run simple examples in CVC5 smt solver. I am missing some core understanding of how pointers and values are treated there and I don't know where to look for more information.

I am sorry for the long snippets, but they are very simple.

First query

(set-logic QF_ALL)
(set-info :smt-lib-version 2.6)

(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :produce-unsat-cores true)

; heap with uninterpreted sort as Data
(declare-sort Data 0)
; "single" element for the pointers to point to
(declare-const unit Data)
; Heap declaration
(declare-heap (Int Data))

; Two pointers
(declare-const left Int)
(declare-const right Int)

; constraints for better readability of the model
(assert (= (as sep.nil Int) 0))
(assert (>= left 0))
(assert (>= right 0))

; query itself
(assert (not 
    (sep
        (pto left unit) 
        (pto right unit)  
    )
))

(check-sat)
(get-model)

CVC5 output

sat
(
; cardinality of Data is 1
; rep: (as @Data_0 Data)
(define-fun unit () Data (as @Data_0 Data))
(define-fun left () Int 1)
(define-fun right () Int 2)
)
(heap
(sep (pto 2 (as @Data_0 Data)) (pto 1 (as @Data_0 Data)))
(= (as sep.nil Int) 0)
)

---

Second query

(set-logic QF_ALL)
(set-info :smt-lib-version 2.6)

(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :produce-unsat-cores true)

; heap with uninterpreted sort as Data
(declare-sort Data 0)
; "single" element for the pointers to point to
(declare-const unit Data)
; Heap declaration
(declare-heap (Int Data))

; Two pointers
(declare-const left Int)
(declare-const right Int)

; constraints for better readability of the model
(assert (= (as sep.nil Int) 0))
(assert (>= left 0))
(assert (>= right 0))

; query itself
(assert  
    (sep
        (pto left unit) 
        (pto right unit)  
    )
)

(check-sat)
(get-model)

CVC5 output

sat
(
; cardinality of Data is 1
; rep: (as @Data_0 Data)
(define-fun unit () Data (as @Data_0 Data))
(define-fun left () Int 1)
(define-fun right () Int 2)
)
(heap
(sep (pto 2 unit) (pto 1 unit))
(= (as sep.nil Int) 0)
)

---

Question about the second heap

(heap
(sep (pto 2 unit) (pto 1 unit))
(= (as sep.nil Int) 0)
)

Why the second heap satisfies (sep (pto left unit) (pto right unit)), despite both pointers pointing to the same unit?

Question about the first heap

(heap
(sep (pto 2 (as @Data_0 Data)) (pto 1 (as @Data_0 Data)))
(= (as sep.nil Int) 0)
)

Why is this heap satisfies not (sep (pto left unit) (pto right unit) even with unit being equal to @Data_0, which works for the other query?

---

Why these similar-looking heaps are satisfying mutually exclusive conditions?

I am looking to some paper or documentation page for the in-depth explanation.

Answer 1

Thanks for the question. The model construction for the separation logic heap in cvc5 was wrong in this case. This will be fixed by https://github.com/cvc5/cvc5/pull/9574.