The backend does not apply simplification rule, while being unable to prove the claim without it

[virgil-serbanuta]

See the end of the issue for some comments. For now, here are some instructions for reproducing the issue:

a.k

module A
  imports BOOL
  imports INT

  syntax A ::= a(Int) | b(Int) | c(Int)
  rule a(X) => b(X)
      requires p1(X modInt 2)
  rule a(X) => b(X)
      requires true
          andBool notBool p1(X modInt 2)
          andBool p2(X modInt 2)
  rule a(X) => b(X)
      requires true
          andBool notBool p1(X modInt 2)
          andBool notBool p2(X modInt 2)
  rule b(X) => c(X)

  syntax Bool ::= p1(Int)  [function, total, no-evaluators]
  syntax Bool ::= p2(Int)  [function, total, no-evaluators]

  syntax Bool ::= definedModInt(Int, Int)  [function, total]
  rule definedModInt (_:Int, X:Int) => X =/=Int 0

  syntax Int ::= Int "modIntTotal" Int  [function, total, klabel(_modIntTotal_), symbol, left, smt-hook(mod)]
  rule _ modIntTotal 0 => 0
  rule X modIntTotal Y => X modInt Y [concrete, simplification]

  rule X modInt Y => X modIntTotal Y
      requires definedModInt(X, Y)
      [simplification, symbolic]
endmodule

proof.k

module PROOF
  imports A

  claim a(X) => c(X)
endmodule

command line:

kompile a.k --backend haskell && kprove proof.k

Output:

  #Not ( {
      false
    #Equals
      p1 ( X modInt 2 )
    }
  #And
    {
      false
    #Equals
      p2 ( X modInt 2 )
    } )
#And
  #Not ( {
      false
    #Equals
      p1 ( X modInt 2 )
    }
  #And
    {
      true
    #Equals
      p2 ( X modInt 2 )
    } )
#And
  #Not ( {
    true
  #Equals
    p1 ( X modInt 2 )
  } )
#And
  <k>
    a ( X ) ~> _DotVar1 ~> .
  </k>

Some comments:

1. This proof works if the rewrite rules for a use modIntTotal instead of modInt.
2. The above most likely happens because the Haskell backend does not send terms that include partial functions to Z3. By this I mean that it replaces the entire { true #Equals p1 ( X modInt 2 ) } term with a variable V and simply sends V to z3. When using modIntTotal, the backend replaces { true #Equals p1 ( X modIntTotal 2 ) } with { true #Equals V } and sends that to z3, which means that z3 has a chance to notice that the entire constraint is unsat.
3. If I try to prove claim b(X modInt 2) => c(X modIntTotal 2), then the backend DOES apply the simplification rule since it finishes the proof successfully. I'm not sure what to make of that.

[virgil-serbanuta]

It turns out that this also works if I change the symbolic attribute to symbolic(X), so this is no longer blocking.

@ehildenb says that symbolic, by itself, means that all arguments must be symbolic. However the documentation (https://kframework.org/docs/user_manual/#concrete-and-symbolic-attributes-(haskell-backend) ) says, in a somewhat ambiguous context, that "Conversely, the symbolic attribute will allow a rule to apply only when some arguments are not concrete." and does nothing else to clarify the slight ambiguity.

So, this may actually be an issue about documentation, not about the backend itself.