Simplification.And.retractLocalFunction: cases for sort inj and builtins

[ana-pantilie]

Fixes #2095

---

Reviewer checklist

• Test coverage: stack test --coverage
• Public API documentation: stack haddock

[ana-pantilie]

With the changes from this PR: test-issue-vote-contract.sh.out.golden
Without the changes: test-issue-vote-contract.sh.out.fail
test-issue-vote-contract.sh.out.zip

[ttuegel]

@sskeirik Could you please verify the output on this one, too?

[sskeirik]

@ttuegel Deciphering the output of kore files is more work to me than just building the PR branch, copying the bins to where my script expects, and re-running my tests. After doing that:

1. I'm still seeing the unsatisfiable branch is not pruned, but with some differences (see below).
2. I'm seeing another unsatisfiable branch that I did not see before

Differences between previous and new version of unsatisfiable branch:

For reference, here is the definition of #lookup a function which wraps map access:

syntax OptionData ::= #lookup(Map, Data, TypeName) [function, smtlib(lookup)]
// --------------------------------------------------------------------------
rule #lookup(M, K, VT) => Some {M[K]}:>Data requires         K in_keys(M) andBool isValue(VT,{M[K]}:>Data)
rule #lookup(M, K, _ ) => None              requires notBool K in_keys(M)

syntax Bool ::= isValue(TypeName, Data)
// ------------------------------------------
rule isValue(int, I:Int) => true
// other equations omitted
// ...

Here is the previous output (with irrelevant constraints omitted):

{ false #Equals I2 +Int 1 ==Int I3 +Int 1 }
{ project:Data(     'QuesUnds'3 [ #SemanticCastToInt ( 'QuesUnds'1 ) ] ) #Equals #SemanticCastToInt ( I2 ) }
{ project:Data(     'QuesUnds'3 [ #SemanticCastToInt ( 'QuesUnds'1 ) ] ) #Equals #SemanticCastToInt ( I3 ) }

Here is the new output (with irrelevant constraints omitted):

(1) { false #Equals I2 +Int 1 ==Int I3 +Int 1 }
(2) { #SemanticCastToInt ( 'QuesUnds'1 ) in_keys('QuesUnds'3) #Equals true }
(3) { project:Data(     'QuesUnds'3 [ #SemanticCastToInt ( 'QuesUnds'1 ) ] ) #Equals #SemanticCastToInt ( I2 ) }
(4) { #lookup( 'QuesUnds'3 , #SemanticCastToInt ( 'QuesUnds'1 ) , int ) #Equals Some #SemanticCastToInt ( I3 ) }
(5) #Ceil( #lookup( 'QuesUnds'3 , #SemanticCastToInt ( 'QuesUnds'1 ) , int ) )
(6) #Ceil( project:Data(     'QuesUnds'3 [ #SemanticCastToInt ( 'QuesUnds'1 ) ] ) )

For some reason, the #lookup function in line (4) is not being simplified to Some project:Data( 'QuesUnds'3 [ #SemanticCastToInt ( 'QuesUnds'1 ) ] by the definition of #lookup and line (2), which would allow generating the equality:

(7) { project:Data(     'QuesUnds'3 [ #SemanticCastToInt ( 'QuesUnds'1 ) ] ) #Equals #SemanticCastToInt ( I3 ) }

New Unsatisfiable Branch

(1) { None #Equals #lookup( 'QuesUnds'3 , #SemanticCastToInt ( 'QuesUnds'1 ) , int ) }
(2) { #SemanticCastToInt ( 'QuesUnds'1 ) in_keys('QuesUnds'3) #Equals true }

By (2) and definition of #lookup, (1) should evaluate to None #Equals Some ... which should be unsatisfiable.

[ana-pantilie]

I'm investigating why #lookup doesn't get evaluated, I'll attach the log with debugging information on equation attempts and applications for this symbol here:
debugLookupEquation.txt

[ttuegel]

Deciphering the output of kore files is more work to me than just building the PR branch, copying the bins to where my script expects, and re-running my tests.

@sskeirik The bug report you submitted with #2095 #2089 doesn't contain any symbol #lookup. Are you using a different version of the semantics? Are you using a different version of the frontend?

@ana-pantilie I'm going to review this as-is and if there are issues remaining, we will deal with those later.

[sskeirik]

@ttuegel I'm not sure 100% sure if everything is exactly the same. I suspect there are differences, though I think they are minor. I haven't had to do a proper debugging session to compare the previous and current versions. If you guys are happy with this, please merge it and I will follow-up when I have time to address this fully.

[ttuegel]

I removed the integration test because it's not evident that it checks what we need it to check.