The “pull-nested-quantifiers” option seems to cause problems in the context for UFBV?

Question

I am currently experimenting with Z3 as bounded engine for specifications written in Alloy (a relational logic/language). I am using the UFBV as target language.

I detect a problem using the Z3 option (set-option :pull-nested-quantifiers true).

For two semantically identical SMT specifications Spec1 and Spec2, Z3 times out (200 sec) for proving Spec1 but proves Spec2.

The only different between Spec1 and Spec2 is that they have different function identifiers (because I use java hash names). Can this be related to a bug?

The second observation I would like to share and discuss, is the "iff" operator in the context of UFBV. This operator is not supported, if (set-logic UFBV) is set. My solution was to use "=" instead but this do not work well if the operands contains deeply nested quantifiers and the "pull-nested-quantifiers" is set. The other saver solution is to use double implication.

Now the question: Is there any other better solution for model "iff" in UFBV, because I think, that using double implication will in general loose maybe useable semantic information for improvement/simplifications.

http://i12www.ira.uka.de/~elghazi/tmp/

you can find: spec1 and spec2 the tow (I think) semantically identical SMT specifications, and spec3 an SMT specification using "=" to model "iff", for which z3 times out.

Answer 1

The default strategy for the UFBV logic is not effective for your problems. Actually, the default strategy solves all of them in less than 1 sec. To force Z3 to use the default strategy, you just need to comment the following lines in your script.

; (set-logic UFBV)
; (set-option :pull-nested-quantifiers true)
; (set-option :macro-finder true)

If the warning messages are bothering you, you can add:

(set-option :print-warning false)

That being said, I will try to address the issues you raised. Does identifier names affect the behavior of Z3? Yes, they do. Starting at version 3.0, we started using a total order on Z3 expressions for performing operations such as: sorting the arguments of associative-commutative operators. This total order is based on the identifier names. Ironically, this modification was motivated by user feedback. In previous versions, we used an internal ID for performing operations such as sorting, and breaking ties in many different heuristics. However, these IDs are based on the order Z3 creates/deletes expressions, which is based on the order users declare symbols. So, Z3 2.x behavior would be affected by trivial modifications such as removing unused declarations.

Regarding iff, it is not part of SMT-LIB 2.0 standard. In SMT-LIB 2.0, = is used for formulas and terms. To make sure Z3 is fully compliant with the SMT-LIB 2.0 standard, whenever users specify a SMT-LIB supported logic (or soon to be supported such as UFBV), Z3 only "loads" the symbols defined in it. When, a logic is not specified, Z3 assumes the user is using the "Z3 logic" that contains all supported theories in Z3, and many extra aliases such as: iff for Boolean =, if for ite, etc.