2
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Maybe try proofassistants.stackexchange.com $\endgroup$
    – Kai
    Commented Feb 27, 2023 at 0:12
  • $\begingroup$ @Kai, thank you, I will try if there are no answers here $\endgroup$
    – FrogOfJuly
    Commented Feb 27, 2023 at 10:17
  • $\begingroup$ @Kai I'm not sure proofassistants is the right place to ask, as long as CVC5 and other SAT/SMT solvers are not proof assistants (they are automatic theorem provers)... $\endgroup$ Commented Feb 27, 2023 at 10:43

1 Answer 1

3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.