I noticed that if I create my own array type that stores bitvectors and assert the first array update axiom, simple assertions afterwards fail to find a solution (my example below neither returns sat nor unsat but just keeps running):
(declare-sort MyArray)
; Indices into the array
(declare-sort Id)
; Returns the value in the array located at the specified index
(declare-fun index
(MyArray Id)
(_ BitVec 8))
; Updates the array so that the provided value is stored at the specified index
(declare-fun upd
(MyArray Id (_ BitVec 8))
MyArray)
; First array update axiom
(assert (forall ((a MyArray) (i Id) (v (_ BitVec 8)))
(=
(index (upd a i v) i)
v)))
(declare-const x Int)
(declare-const y Int)
(echo "")
(echo "Sanity check, should be sat:")
(assert (= x y))
(check-sat)
However, if I instead specify that my array stores a custom sort z3 finds a solution very quickly:
(declare-sort MyArray)
; Indices into the array
(declare-sort Id)
; Values stored in the array
(declare-sort Elem)
; Returns the value in the array located at the specified index
(declare-fun index
(MyArray Id)
Elem)
; Updates the array so that the provided value is stored at the specified index
(declare-fun upd
(MyArray Id Elem)
MyArray)
; First array update axiom
(assert (forall ((a MyArray) (i Id) (v Elem))
(=
(index (upd a i v) i)
v)))
(declare-const x Int)
(declare-const y Int)
(echo "")
(echo "Sanity check, should be sat:")
(assert (= x y))
(check-sat)
Does anyone know why this is the case? It's possible that z3 gets caught in some kind of instantiation loop (since the upd function both takes and returns MyArray sort), but I'm surprised that it only seems to get tripped up with bitvectors as the elements. Is this related to Nikolaj's answer that the quantifier elimination tactic is currently fairly simplistic when it comes to bit-vectors?
I'm using bitvectors because my problem ultimately involves some bitvector operations (especially bvxor). Is it better just to define my own operations and essentially recreate part of the theory of bitvectors? Or is there a better way to go about this (than mixing quantifiers, bitvectors, and part of the theory of arrays)? I'm really just interested in operations on bytes so all my bitvectors are of length 8.
I don't think there's a good reason why z3 is not terminating on the first program you gave here. Running with z3 -v:10 suggests it gets into some sort of an unproductive loop, that the second version avoids. I think you should report this at https://github.com/Z3Prover/z3/issues. Even though it's not strictly speaking a "bug," it's surprising behavior and the developers might want to look at it. (Please report back what you find.)
Regarding your second question: Do not reinvent what z3 already has support for! Use the internal arrays; they have a custom decision procedure and it has gone years of tuning. The introduction of quantified axioms will no doubt create more work than is necessary. Does something go wrong if you use internal arrays? Why would you not use them anyhow? Only look at your own axiomatization, if the internal built-in one isn't working well. (Even then, I'd first check with developers to see why.)