problematic interaction between macro-finder and arrays (z3-py)

[jesboat]

Given the following Python input:

from z3 import *

Z = IntSort()

f1 = Function('f1', Z, Z)
f2 = Function('f2', Z, Z)

arr = Const('arr', ArraySort(Z, Z))
val = Const('val', Z)

s = Solver()
s.set(macro_finder=True)
s.add(
    ForAll([val],
        f2(val) == f1(val)),
    f2(arr[0]) == 42,
    Map(f2, arr) == K(Z, 23),
)

print(s.check())
print(s.model().eval(Map(f2, arr) == K(Z, 23)))

We get

sat
False

So Z3 finds what it thinks is a model, but even the model itself can tell one of the assertions is violated.

I haven't been able to simplify this further, or get a repro with smtlib input.

Tested using z3_solver-4.10.2.0 on an M1 mac, and with a debug build on 49064252acd664b8dedecbb95a6f883650a00891 on the same machine.

[NikolajBjorner]

macro-finder never worked with operations that use function symbols as arguments: as-array and map. It also doesn't work when you have recursive functions. It is used only sparingly in internal scenarios. To fix it to be safe, or auto-disable it, generally would require some heavy lifting (it isn't a simple bug fix).

[jesboat]

Wow, that was an amazingly fast response and patch. Thank you for that, and for the details!

To fix it to be safe, or auto-disable it, generally would require some heavy lifting (it isn't a simple bug fix).

I did see that MF disables itself in the presence of recfuns, and it looks like your commit just now will (if I'm understanding correctly) expand macros in the places where they're applied, but preserve the original defining formulae for map/as-array to see.

Does that mean that MF will now be safe to have enabled? (in master). Or do you mean that there are probably some other correctness issues which would be hard to fix?

[NikolajBjorner]

Does that mean that MF will now be safe to have enabled? (in master). Or do you mean that there are probably some other correctness issues which would be hard to fix?

From what I can say it is now safe for arrays map/as-array.

When z3 does dirty tricks with functions elsewhere it will not be safe. Probably the other place is for transitive closure of relations. This is a niche feature, so chasing it seems to be more a risk of introducing a regression than fixing anybody's problem. Z3 should not do these dirty tricks, at arbitrary places, but this requires a structural change.

Given that you seem to have an application (regex puzzles?) and not just poking around for mistakes I went ahead to address the bug. We would like to incentivize sharing fun applications that can serve as tutorials under https://microsoft.github.io/z3guide/. It can perhaps be added using a pull request under programming z3 as read-only code.

[jesboat]

Cool, I'll take a look at that. Thank you!

Right now, I've been poking around with modeling semantics of some very simple programing languages (not even Turing-complete). I'm ending up with a bunch of quantifiers though (many of them are for things MF eliminates) and since sometimes I'm looking for a model, I have to keep MBQI on (AIUI) so without MF, things get very clunky very fast. (I've tried inlining the functions on the Python side, but the formulae getting passed to Z3 end up getting kinda huge.)

The regex-crosswords didn't need quantifiers and Z3 munched through that with no sweat at all :)

Again, thanks for the fast response.