Allow including lemmas dynamically into APRProver

[ehildenb]

In order to include lemmas dynamically in the Kontrol prover, we need an option for passing the extra module into the APRProver so that it can be fed into the booster's add-module endpoint. This also requires being able to translate functional rules to Kore in pyk using krule_to_kore. This PR:

• Adds the extra_module parameter to the APRProver initialization, which allows passing a new module with lemmas into the prover at initialization time. It will pass this module on to the add-module endpoint and make sure it's used on all future requests.
• Adds the symbolic and smt-lemma attributes to the list of attributes recognized by pyk.
• Renames KProve.get_claims_modules to KProve.parse_modules, and renames some of its parameters.
• Adds support to specifying the sort to use in bool_to_ml_pred for converting boolean predicates to matching logic ones.
• Makes adjustments to _krule_to_kore to make it support translating some functional/simplification rules to Kore which were not supported before (and adds tests):
  • Factors out _krule_att_to_kore method for converting attributes of KRule to kore.
  • Adds a pass to process the rule attributes a bit in krule_to_kore (eg. handle owise => priority(200) and simplification vs priority).
  • Sort the attributes before sending to Kore (for reliable ordering of the Kore output).
  • Refactors the production of Kore axiom to differentiate between semantic and functional rules, and to convert functional rules as matching-logic implies axioms.

[palinatolmach]

Suggested change