tracking: rewriting

[c-cube]

• conditional rewriting

  • parse rewrite forall vars. ∧_i a_i => l = r

  • same for clausal rewriting

  • handling by inference rule that unifies (rewrite & narrowing are the same)

    `∧_i a_i => l = r           C[l]    lσ=a
    ----------------------------------------
        ∧_i a_iσ => C[rσ]
    

    which is a form of superposition that is artificially restricted to
    rewriting l first

  • for each rule, compile fast pre-checks (e.g.
    matched term must have symbol f at arg position i) and use
    these before attempting call to matching

  • in proof, put set of rewrite rules used in simplification steps,
    at least in full (non-compressed) version