Polymorphic arrays

[mezpusz]

Changed arrays to be polymorphic w.r.t. their index and inner sorts.

This allowed me to also remove the infamous MonomorphisedInterpretation and some related dead code.

[mezpusz]

No changes according to regression over TPTP.

[MichaelRawson]

Nice, but a few questions:

1. What now happens with an array of Booleans and ARRAY_BOOL_SELECT? Are these now pseudo-Booleans?
2. How does the interpretation of equality work? See comment inline.
3. Don't we need to change the array theory code (if any exists) to expect 5 arguments, not 3?
4. Is it worth a run on some chunk of SMT-LIB? I think arrays were already (slightly) broken, but we might now be better or worse.

[MichaelRawson]

Could this have a comment saying roughly what it does in various cases? Especially equality, array functions, array functions on Booleans, ...

[mezpusz]

Sure, I will add a comment!

[quickbeam123]

This is probably still a TODO?

[mezpusz]

I added comments for equality and the array operators, not sure if the others need explaining (and if yes, maybe I'm not the authority to add comments to those).

[mezpusz]

1. What now happens with an array of Booleans and ARRAY_BOOL_SELECT? Are these now pseudo-Booleans?

Yes, I think it's not worth it adding them separately, given that no one seems to be interested in array reasoning in Vampire at the moment. We can change it back when needed!

2. How does the interpretation of equality work? See comment inline.

This comes from here originally, I just moved it to the common place for all interpreted stuff.

3. Don't we need to change the array theory code (if any exists) to expect 5 arguments, not 3?

I think I did and there were only axioms regarding arrays, but let me know if you find any other place where they are used!

4. Is it worth a run on some chunk of SMT-LIB? I think arrays were already (slightly) broken, but we might now be better or worse.

Probably yes, I will look the related fragments up and give it a try!

[MichaelRawson]

I think I did and there were only axioms regarding arrays

Yeah, I couldn't find anything else from a quick look. Thanks!

[mezpusz]

It was a good call to run SMTLIB..

I ran with -sa discount -i 20000 all 38217 benchmarks that claim to be related to arrays. In particular, ALIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA and AUFNIRA. There were almost 20k benchmarks where both master and this branch crashed due to an unrelated bug introduced with the let-bound PR a few weeks ago. So I would first fix that so we see clearly, and rerun this without the big diff.

[MichaelRawson]

Thanks for looking into it! Good that you caught this, and the plan sounds good to me.

[MichaelRawson]

Is this now ready to go again once merge conflicts are fixed?

[mezpusz]

Still gonna run a regression over SMTLIB to see what changed...

Update:

TPTP discount:
master unsat: 10247 (0) sat: 1030 (0)
branch unsat: 10247 (0) sat: 1030 (0)

TPTP otter:
master unsat: 10300 (1) sat: 1020 (0)
branch unsat: 10299 (0) sat: 1020 (0)

induction:
master unsat: 959 (4) sat: 0 (0)
branch unsat: 963 (8) sat: 0 (0)

synthesis:
master unsat: 437 (0) sat: 0 (0)
branch unsat: 437 (0) sat: 0 (0)

SMTLIB discount:
TBD

[mezpusz]

With SMTLIB there is some trouble:

master unsat: 54782 (259) sat: 258 (0)
branch unsat: 54649 (126) sat: 258 (0)

I'll look into it when I have some time.

UPDATE:

Inspecting some proofs I believe we lose problems because of the increased complexity of dealing with polymorphic symbols instead of monomorphic ones:

• In many cases the proofs look very similar, but clauses are selected much later due to the increased weight and more variable occurrences.
• In some cases we get extra unnecessary FOOL reasoning due to Boolean arrays not being Literals anymore.

We should weigh now how much we want this more efficient monomorphised reasoning for arrays in particular, given the extra code complexity that it comes with.

[MichaelRawson]

I'm not so fussed about stuff lost for "heuristic" reasons like term weights. We could probably bring these back by some strategy scheduling, and failing that by introducing a flag for ignoring sort weight if that doesn't exist already.

Unnecessary FOOL reasoning is more annoying, but perhaps this is the moment to do "Boolean promotion to literals" as a preprocessing step?

[mezpusz]

Unnecessary FOOL reasoning is more annoying, but perhaps this is the moment to do "Boolean promotion to literals" as a preprocessing step?

I'm not sure how this would be done, but sure, we can start thinking about it. It would make sense in the higher-order context too.

[MichaelRawson]

Could you give an example of the unnecessary FOOL reasoning you encountered?

[mezpusz]

For example, AUFDTLIRA/20200306-Kanig/spark2014bench/P503-001__bitsets__bitsets.ads_19_9_test_main.adb_5_4_postcondition___00.smt2 contains now things like the following in the proof:

184. ($true != $select($int,$o,X3,X2)) | 1 = iG2(X2,X3) [cnf transformation 130]
185. ($true = $select($int,$o,X1,X0)) | 0 = iG2(X0,X1) [cnf transformation 130]
214. ~mem(X0,X1) | ($select($int,$o,X0,X1) = $true) [cnf transformation 154]
215. ($select($int,$o,X0,X1) != $true) | mem(X0,X1) [cnf transformation 154]

whereas before it was:

172. ($true = bG9) | 1 = 0 [cnf transformation 143]
200. ~$select($store(X1,X3,X0),X2) | $select(X1,X2) | X2 = X3 [cnf transformation 152]
232. ~mem(X0,X1) | $select(X0,X1) [cnf transformation 165]
233. ~$select(X0,X1) | mem(X0,X1) [cnf transformation 165]

(I think I copied not exactly one-to-one corresponding parts.) Not sure though how much this is actually the culprit, but it certainly complicates saturation a bit.

[MichaelRawson]

Yuck, that looks uglier than I hoped. I was expecting to do something like

$$select_bool(Sort, Array, Index) <=> $select(Sort, Array, Index) = $true

and get back to something neater, but the more I think about it the less that makes sense to me. I'm certainly OK with it how it is, though.

[mezpusz]

No, we don't treat such Booleans in any special way, as far as I know.