Core inference unit tests

[mezpusz]

Added unit tests to most of the testable core inferences.

Coverage change:

	master	branch
Lines	35.5%	40.0%
Functions	53.4%	55.5%
Branches	20.6%	22.9%

Regression over FOL showed no difference.

[MichaelRawson]

No objection to more unit testing, and some cleanup too! Hopefully promoting inner rewriting to an immediate simplification should be profitable too.

[mezpusz]

Hopefully promoting inner rewriting to an immediate simplification should be profitable too.

There is actually some interesting conclusion on that part. I ran regression with -irw on and I got the following (run 0 = master, run 1 = this branch):

Discount:

run 0 unsat: 9207 (20) sat: 1031 (1) cputime: 56746.40 s instructions: 222833569 Mi memory: 1532081.48 MB
run 1 unsat: 9204 (17) sat: 1032 (2) cputime: 56838.31 s instructions: 222905021 Mi memory: 1532898.89 MB

run 0 uniquely proved: 20
SET/SET515-6.p
SWC/SWC055-1.p
SWC/SWC056-1.p
SWC/SWC077-1.p
SWC/SWC249-1.p
SWV/SWV282-2.p
SYN/SYN076-1.p
ALG/ALG032+1.p
GEO/GEO500+1.p
NUM/NUM586+1.p
NUM/NUM588+1.p
NUM/NUM607+1.p
PUZ/PUZ133+2.p
SCT/SCT168+1.p
SEU/SEU293+2.p
SWC/SWC188+1.p
SWC/SWC314+1.p
SWC/SWC421+1.p
SWV/SWV474+1.p
ITP/ITP375_1.p

run 0 uniquely disproved: 1
KLE/KLE176+1.p

run 1 uniquely proved: 17
NUM/NUM058-1.p
SWC/SWC107-1.p
SWC/SWC113-1.p
SWC/SWC123-1.p
SWV/SWV712-1.p
GEO/GEO287+1.p
GRA/GRA006+1.p
KLE/KLE027+1.p
LAT/LAT287+1.p
NUM/NUM430+1.p
NUM/NUM566+3.p
NUM/NUM595+1.p
NUM/NUM924+2.p
SEU/SEU290+2.p
SWC/SWC014+1.p
SWW/SWW219+1.p
ITP/ITP004_7.p

run 1 uniquely disproved: 2
LAT/LAT395-1.p
KLE/KLE178+1.p

Otter:

run 0 unsat: 9311 (32) sat: 1021 (0) cputime: 61550.20 s instructions: 223054932 Mi memory: 1739472.98 MB
run 1 unsat: 9299 (20) sat: 1021 (0) cputime: 61716.66 s instructions: 223122064 Mi memory: 1738134.16 MB

run 0 uniquely proved: 32
COL/COL038-1.p
GRP/GRP401-1.p
LAT/LAT237-1.p
SET/SET505-6.p
SWC/SWC113-1.p
ALG/ALG032+1.p
CSR/CSR001+1.p
GEO/GEO499+1.p
KLE/KLE027+1.p
KLE/KLE027+2.p
KLE/KLE027+3.p
KLE/KLE041+1.p
LAT/LAT287+1.p
LAT/LAT340+1.p
LAT/LAT361+1.p
NUM/NUM461+2.p
NUM/NUM465+1.p
NUM/NUM478+2.p
NUM/NUM513+3.p
NUM/NUM558+3.p
NUM/NUM926+7.p
NUM/NUM926+8.p
RNG/RNG119+4.p
SEU/SEU208+2.p
SEU/SEU430+2.p
SWC/SWC014+1.p
SWC/SWC327+1.p
SWC/SWC343+1.p
SWV/SWV125+1.p
DAT/DAT050_1.p
SWX/SWX083_1.p
SWV/SWV739_5.p

run 0 uniquely disproved: 0

run 1 uniquely proved: 20
SET/SET195-6.p
SET/SET497-6.p
SWV/SWV716-1.p
SWV/SWV776-1.p
ALG/ALG226+1.p
COM/COM142+1.p
CSR/CSR002+1.p
GEO/GEO277+1.p
KLE/KLE010+2.p
LAT/LAT324+1.p
NUM/NUM516+1.p
NUM/NUM536+1.p
NUM/NUM588+1.p
NUM/NUM629+1.p
SEU/SEU203+2.p
SEU/SEU444+2.p
SWC/SWC072+1.p
SWC/SWC087+1.p
ITP/ITP011_2.p
LCL/LCL808_5.p

run 1 uniquely disproved: 0

So it gets a bit worse, but at least now it is properly done where it needs to be (IMO). If we can't live with these, I can revert the changes!

[quickbeam123]

So it gets a bit worse, but at least now it is properly done where it needs to be (IMO). If we can't live with these, I can revert the changes!

This is suspicious...

Let's assume that InnerRewriting is expensive. Then we only want to try it when all other simplification attempts failed. Maybe it would better be inserted first (and not last), given that the CompositeISE behaves like a stack?

Could you please test this other option using the same setup?

[mezpusz]

Interestingly, I get almost the same result with InnerRewriting being at the end of the simplifiers. Let me know if I should revert changing it to an ImmediateSimplificationEngine.