Allow including lemmas dynamically into APRProver#4681

Merged

rv-jenkins merged 29 commits intodevelopfrom custom-modules-for-proofs

Nov 21, 2024

+231-65

Commits on Nov 9, 2024

Commits on Nov 10, 2024

pyk/kast/manip: allow bool_to_ml_pred to specify the target sort
ehildenb
committed
pyk/konvert/_kast_to_kore: allow translating functional rules from Kast to Kore
ehildenb
committed
pyk/tests/integration/k-files/simple-proofs.k: add more examples of functional rules to translate
ehildenb
committed
pyk/konvert/_kast_to_kore: factor out attribute konversion
ehildenb
committed
pyk/konvert/_kast_to_kore: add support for converting SIMPLIFICATION attribute
ehildenb
committed
pyk/kast/att: add smt-lemma and symbolic attributes
ehildenb
committed
pyk/konvert/kast_to_kore: support more translation of kast attributes to kore
ehildenb
committed
pyk/kast/outer: typo in comment
ehildenb
committed
pyk/tests/integration/{simple-proofs.k,test_simple_proofs.py}: update tests to working version
ehildenb
committed
pyk/konvert/_kast_to_kore: correctly handle conversion of variables in concrete/symbolic attribute too
ehildenb
committed

Commits on Nov 13, 2024

pyk/konvert/_kast_to_kore: make sure to sort attribute entries first
ehildenb
committed