Support for AUFBV?

Will Z3 be supporting AUFBV?

For the following script:

(set-logic AUFBV)
(declare-fun x () (_ BitVec 16))
(declare-const t (Array (_ BitVec 16) (_ BitVec 16)))
(assert (= (select t #x00开发者_C百科00) #x0000))

The online Z3 demo seems to be happy with the set-logic call, but then it complains about the sorts BitVec and Array. (Incidentally, the online demo seems to be happy with the set-logic call regardless of the logic name, even with bogus names such as (set-logic blarg).)

The SMT-Lib web-site does not mention neither UFBV nor AUFBV, but given their quantifier-free counterparts (QF_UFBV and QF_AUFBV), I was hoping Z3 would support AUFBV as well.

Needless to say, arrays play a very important role in practice. I think the AUFBV logic should remain decidable given the finiteness argument. It'd be really nice to see Z3 support it.

Thanks!

Z3 uses the set-logic command to configure itself. If a SMT script does not contain the set-logic then all theory solvers are enabled. If you remove the set-logic command from your script, then Z3 will work as expected.

As you said, the AUFBV logic is decidable. However, the complexity is really high (NEXPTIME-complete). In theory, the Model Based Quantifier Instantiation (MBQI) module guarantees that Z3 is a decision procedure for this logic, but due to the high complexity, Z3 will fail (run without memory and/or time) in many scripts.

The logic AUFBV is not in the list of officially supported logics. Z3 did not recognized it, and did not install any theory solver. So, to use this logic in Z3 3.1, you should not use the set-logic command.

BTW, you don't really need arrays. They can be encoded in UFBV using quantifiers. In many cases, if one is using quantifiers, it is best to avoid the array theory. The array theory solver in Z3 is optimized for quantifier-free problems.

Regarding bogus commands such as (set-logic blarg), I added code for displaying a warning message saying the logic was not recognized, and Z3 will use all available theories. The modification will be available in Z3 3.2. I also included AUFBV in the list of officially supported logics.