Remove Kore.Internal.SideCondition.andCondition

[andreiburdusa]

---

Fixes #1733

Reviewer checklist

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

[andreiburdusa]

What I learned from running functions/positive-spec.k in the repl, both before and after removing andCondition:

Both go to node 1 the same way, using Axiom 0.

Then, from node 1:

  <T>
    <k> next true </k>
    <n> N:Int </n>
  </T>
#And { N >Int 0 #Equals true }

both use Claim 0:

  #Ceil ( positive ( N ) )
#And
  <T>
    <k> next positive ( N ) </k>
    <n> N:Int </n>
  </T>

→ ◇w

<T>
  <k> end </k>
  <n> N:Int </n>
</T>

But instead of getting node 2 with the configuration

  <T>
    <k> end </k>
    <n> N:Int </n>
 </T>
#And { N >Int 0 #Equals true }

After removing andCondition it gets node 2:

  #Ceil ( positive ( N ) )
#And
  <T>
    <k> end </k>
    <n> N:Int </n>
  </T>
#And { N >Int 0 #Equals true }
#And { true #Equals positive ( N ) }

I think the difference is in applying the rule

rule positive(M) => true
  requires M >Int 0

[ttuegel]

We should check the call sites of applyEquation to see what SideCondition it is called with.

[ttuegel]

We should check the call sites of applyEquation to see what SideCondition it is called with.

Sorry, I meant attemptEquation here.

[andreiburdusa]

We should check the call sites of applyEquation to see what SideCondition it is called with.

Sorry, I meant attemptEquation here.

Is this the SideCondition we are looking for?

\and{_PREDICATE{}}(
    /* term: */
    /* D Sfa */ \top{_PREDICATE{}}(),
\and{_PREDICATE{}}(
    /* predicate: */
    /* Sfc */
    \ceil{SortBool{}, _PREDICATE{}}(
        /* Fn Sfc */
        Lblpositive'LParUndsRParUnds'FUNCTIONS'Unds'Bool'Unds'Int{}(
            /* Fl Fn D Sfa */ VarN:SortInt{}
        )
    ),
    /* substitution: */
    /* Spa */
    \equals{SortGeneratedCounterCell{}, _PREDICATE{}}(
        /* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{},
        /* Fl Fn D Sfa */
        Lbl'-LT-'generatedCounter'-GT-'{}(
            /* Fl Fn D Sfa */ VarDotVar00:SortInt{}
        )
    )
))

It's passed to attemptEquation inside definitionEvaluation

[ttuegel]

The problem is because we do not pass in a SideCondition when applying a semantic rule. The constraint

true #Equals positive ( N )

originates when we apply the claim next positive(N) => end to the configuration next true. We need to use the top-level SideCondition

N >Int 0 #Equals true

when we simplify the positive constraint. The backend does not yet support re-simplifying the top-level SideCondition with itself, so we have to complete the simplification of positive before we add that constraint to the top-level SideCondition (that is: before we finish applying the claim).

[andreiburdusa]

Now there is only one unit test failing.

The reason is that the rule

claim {}
/* Spa */
    \implies{testSort{}}(
        /* Spa */
        \and{testSort{}}(
            /* Spa */
            \equals{testSort{}, testSort{}}(
                /* Fl Fn D Sfa */ x:testSort{},
                /* Fl Fn D Sfa Cl */ a{}()
            ),
            /* Fl Fn D Sfa */ x:testSort{}    <---- this is the only difference
        ),
        /* Spa */
        weakExistsFinally{testSort{}}(
            /* Spa */
            \and{testSort{}}(
                /* Spa */
                \not{testSort{}}(
                    /* Spa */
                    \equals{testSort{}, testSort{}}(
                        /* Fl Fn D Sfa */ x:testSort{},
                        /* Fl Fn D Sfa Cl */ a{}()
                    )
                ),
                /* Fl Fn D Sfa */ x:testSort{}
            )
        )
    )
[]

becomes

    claim {}
    /* Spa */
        \implies{testSort{}}(
            /* Spa */
            \and{testSort{}}(
                /* Spa */
                \equals{testSort{}, testSort{}}(
                    /* Fl Fn D Sfa */ x:testSort{},
                    /* Fl Fn D Sfa Cl */ a{}()
                ),
                /* Fl Fn D Sfa Cl */ a{}()    <---- this is the only difference
            ),
            /* Spa */
            weakExistsFinally{testSort{}}(
                /* Spa */
                \and{testSort{}}(
                    /* Spa */
                    \not{testSort{}}(
                        /* Spa */
                        \equals{testSort{}, testSort{}}(
                            /* Fl Fn D Sfa */ x:testSort{},
                            /* Fl Fn D Sfa Cl */ a{}()
                        )
                    ),
                    /* Fl Fn D Sfa */ x:testSort{}
                )
            )
        )
    []

when given as an argument to runOnePathSteps

I think requires is applied to left.

[ttuegel]

This is fine for now, but let's make a follow-up pull request to add a SideCondition argument to simplifyAnds and remove this topTODO.