Inconsistent behaviour regarding extensionality of maps

Jul 16, 2014 at 8:37 PM
Edited Jul 16, 2014 at 8:39 PM
Hi,

I recently discovered that Boogie behaves in an inconsistent way when it comes to the extensionality of Maps (extensionality is considering two maps to be equal if they contain the same elements).

Consider the following program
procedure main()
{
    var a:[int]int;
    var b:[int]int;

    assume (forall x:int :: a[x] == b[x]);
    assert a == b;
}
If I ask Boogie to verify this program using its default flags it claims that assertion might be violated.

However if I use the /useArrayTheory command line flag to Boogie it now considers this program correct.

According to the "This is Boogie 2" document Maps in Boogie don't have extensionality however we can see if we use the right flag with Boogie is does seem to think Maps have extensionality.

I believe the underlying issue is
  • With the /useArrayTheory flag. The Array theory is used to represent Maps in the SMTLIBv2 query and in this theory Arrays are considered to have the property of extensionality
  • Without this flag maps are encoded as uninterpreted functions in the SMTLIBv2 like so...

(declare-sort |T@[Int]Int| 0)
(declare-fun |Select_[$int]$int| (|T@[Int]Int| Int) Int)
(declare-fun a () |T@[Int]Int|)
(declare-fun b () |T@[Int]Int|)
...
; The assume ends up in the assertions...
(forall ((x Int) ) (! (= (|Select_[$int]$int| a x) (|Select_[$int]$int| b x))
...
; Burried somewhere in the assertion is our assertion from the Boogie program
(= a b)
I presume (= a b) can evaluate to false seeing as it has not been defined what it means for these custom sorts ( |T@[Int]Int|) to be equal.


Is this behaviour intentional?
Jul 27, 2014 at 12:32 AM
Good luck getting your question answered! I find the level of support in this discussion group to be quite poor, unfortunately. Your best bet is to fish through the source code and hope you can get to the source of the problem
Aug 10, 2014 at 1:20 AM
Yes, the incompleteness in Boogie without /useArrayTheory is intentional. I have observed the standard tradeoff of incompleteness for better performance in many situations.