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.
