Fix solver logic to QF_LIA

[senier]

Description

This just fixes the solver logic to QF_LIA without changing types bit vectors as planned originally. For checking all example specifications we observe a 50-fold speedup. I have an initial conversion to bitvectors, but there were still thirty failing tests. I don't think this big change is justified given the speedup we get by just fixing the logic.

EDIT: I forgot to clean the cache. We also need QF_NIA, as QF_LIA does not support *, /, mod etc. The actual speedup is between 3% and 11%. Consequently, the BV changes in #612 and #625 may still be useful.

@treiher Please try with your DHCP example.

[treiher]

I get a long list of errors for DHCP after this change:

specs/dhcp.rflx:163:18: model: error: unreachable field "Len" in "DHCP::Option"
specs/dhcp.rflx:163:18: model: info: path 0 (Code -> Len):
specs/dhcp.rflx:180:18: model: error: unreachable field "Cookie_Servers" in "DHCP::Option"
specs/dhcp.rflx:180:18: model: info: path 0 (Code -> Len -> Cookie_Servers):
specs/dhcp.rflx:176:18: model: error: unreachable field "Domain_Name_Servers" in "DHCP::Option"
specs/dhcp.rflx:176:18: model: info: path 0 (Code -> Len -> Domain_Name_Servers):
specs/dhcp.rflx:184:18: model: error: unreachable field "Impress_Servers" in "DHCP::Option"
specs/dhcp.rflx:184:18: model: info: path 0 (Code -> Len -> Impress_Servers):
specs/dhcp.rflx:182:18: model: error: unreachable field "LPR_Servers" in "DHCP::Option"
specs/dhcp.rflx:182:18: model: info: path 0 (Code -> Len -> LPR_Servers):
specs/dhcp.rflx:178:18: model: error: unreachable field "Log_Servers" in "DHCP::Option"
specs/dhcp.rflx:178:18: model: info: path 0 (Code -> Len -> Log_Servers):
specs/dhcp.rflx:174:18: model: error: unreachable field "Name_Servers" in "DHCP::Option"
specs/dhcp.rflx:174:18: model: info: path 0 (Code -> Len -> Name_Servers):
specs/dhcp.rflx:256:18: model: error: unreachable field "NetBIOS_Over_TCP_IP_Datagram_Distribution_Servers" in "DHCP::Option"
specs/dhcp.rflx:256:18: model: info: path 0 (Code -> Len -> NetBIOS_Over_TCP_IP_Datagram_Distribution_Servers):
specs/dhcp.rflx:254:18: model: error: unreachable field "NetBIOS_Over_TCP_IP_Name_Servers" in "DHCP::Option"
specs/dhcp.rflx:254:18: model: info: path 0 (Code -> Len -> NetBIOS_Over_TCP_IP_Name_Servers):
specs/dhcp.rflx:248:18: model: error: unreachable field "Network_Information_Servers" in "DHCP::Option"
specs/dhcp.rflx:248:18: model: info: path 0 (Code -> Len -> Network_Information_Servers):
specs/dhcp.rflx:250:18: model: error: unreachable field "Network_Time_Protocol_Servers" in "DHCP::Option"
specs/dhcp.rflx:250:18: model: info: path 0 (Code -> Len -> Network_Time_Protocol_Servers):
specs/dhcp.rflx:214:18: model: error: unreachable field "Path_MTU_Plateau_Table" in "DHCP::Option"
specs/dhcp.rflx:214:18: model: info: path 0 (Code -> Len -> Path_MTU_Plateau_Table):
specs/dhcp.rflx:206:18: model: error: unreachable field "Policy_Filter" in "DHCP::Option"
specs/dhcp.rflx:206:18: model: info: path 0 (Code -> Len -> Policy_Filter):
specs/dhcp.rflx:186:18: model: error: unreachable field "Resource_Location_Servers" in "DHCP::Option"
specs/dhcp.rflx:186:18: model: info: path 0 (Code -> Len -> Resource_Location_Servers):
specs/dhcp.rflx:170:18: model: error: unreachable field "Routers" in "DHCP::Option"
specs/dhcp.rflx:170:18: model: info: path 0 (Code -> Len -> Routers):
specs/dhcp.rflx:230:18: model: error: unreachable field "Static_Routes" in "DHCP::Option"
specs/dhcp.rflx:230:18: model: info: path 0 (Code -> Len -> Static_Routes):
specs/dhcp.rflx:172:18: model: error: unreachable field "Time_Servers" in "DHCP::Option"
specs/dhcp.rflx:172:18: model: info: path 0 (Code -> Len -> Time_Servers):
specs/dhcp.rflx:457:29: parser: error: undefined element type "DHCP::Option"
specs/dhcp.rflx:480:10: model: error: missing type for field "Options" in "DHCP::Message"

The specification can be found here.

[senier]

I get a long list of errors for DHCP after this change:

This was due to using the wrong logic. I changed this in 73431da. I also added slightly more useful error messages in those cases in e2ef93c. See the updated PR description - the performance improvement is not at all as impressive as I thought.

[treiher]

Consequently, the BV changes in #612 and #625 may still be useful.

The commit message of 73431da still closes both issues. Is that intended?

[senier]

Consequently, the BV changes in #612 and #625 may still be useful.

The commit message of 73431da still closes both issues. Is that intended?

No, changed in d246337.

[senier]

@treiher I had to refactor the PR a bit to achieve test coverage. The logic became a parameter to the constructor of the Proof class so we can set it to an unsuitable logic in the tests and trigger the UNKNOWN issue.

[senier]

@treiher Rebased to current main.