Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Allow including lemmas dynamically into APRProver #4681

Open
wants to merge 24 commits into
base: develop
Choose a base branch
from
Open

Allow including lemmas dynamically into APRProver #4681

wants to merge 24 commits into from

Commits on Nov 9, 2024

  1. pyk/ktool/{claim_loader,kprove}: rename KProve.{get_claim_modules => … 

    …parse_modules}
    @ehildenb
    ehildenb committed Nov 9, 2024
    Configuration menu
    Copy the full SHA
    a87d5de View commit details
    Browse the repository at this point in the history

  2. pyk/konvert/_kast_to_kore: minor refactoring

    @ehildenb
    ehildenb committed Nov 9, 2024
    Configuration menu
    Copy the full SHA
    fc07a70 View commit details
    Browse the repository at this point in the history

  3. pyk/tests/konvert/test_simple_proofs: add failing test of konverting … 

    …a functional rule
    @ehildenb
    ehildenb committed Nov 9, 2024
    Configuration menu
    Copy the full SHA
    be60d21 View commit details
    Browse the repository at this point in the history

  4. pyk/kast/outer: add simple table of function labels to KDefinition

    @ehildenb
    ehildenb committed Nov 9, 2024
    Configuration menu
    Copy the full SHA
    967b79a View commit details
    Browse the repository at this point in the history

  5. pyk/konvert/_kast_to_kore: support simple translation of functional r… 

    …ules to kore
    @ehildenb
    ehildenb committed Nov 9, 2024
    Configuration menu
    Copy the full SHA
    dd4a8b3 View commit details
    Browse the repository at this point in the history

  6. pyk/tests/integration/konvert/test_simple_proofs: sss

    @ehildenb
    ehildenb committed Nov 9, 2024
    Configuration menu
    Copy the full SHA
    a1b6e4d View commit details
    Browse the repository at this point in the history

  7. pyk/tests/integration/konvert/test_simple_proofs: add test of require… 

    …s clause translation for functional rule
    @ehildenb
    ehildenb committed Nov 9, 2024
    Configuration menu
    Copy the full SHA
    2f7fe10 View commit details
    Browse the repository at this point in the history

  8. pyk/tests/integration/konvert/test_simple_proofs: add test of simplif… 

    …ication rules to konvert
    @ehildenb
    ehildenb committed Nov 9, 2024
    Configuration menu
    Copy the full SHA
    30c4274 View commit details
    Browse the repository at this point in the history

  9. pyk/tests/integration/konvert/test_simple_proofs: priority attribute … 

    …after others
    @ehildenb
    ehildenb committed Nov 9, 2024
    Configuration menu
    Copy the full SHA
    8092e50 View commit details
    Browse the repository at this point in the history

Commits on Nov 10, 2024

  1. pyk/kast/manip: allow bool_to_ml_pred to specify the target sort

    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    d3ccdfe View commit details
    Browse the repository at this point in the history

  2. pyk/konvert/_kast_to_kore: allow translating functional rules from Ka… 

    …st to Kore
    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    8dbaa74 View commit details
    Browse the repository at this point in the history

  3. pyk/tests/integration/k-files/simple-proofs.k: add more examples of f… 

    …unctional rules to translate
    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    7492dd1 View commit details
    Browse the repository at this point in the history

  4. pyk/konvert/_kast_to_kore: factor out attribute konversion

    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    1ba2eec View commit details
    Browse the repository at this point in the history

  5. pyk/konvert/_kast_to_kore: add support for converting SIMPLIFICATION … 

    …attribute
    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    d33b9bc View commit details
    Browse the repository at this point in the history

  6. pyk/kast/att: add smt-lemma and symbolic attributes

    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    183044a View commit details
    Browse the repository at this point in the history

  7. pyk/konvert/kast_to_kore: support more translation of kast attributes… 

    … to kore
    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    d091d9d View commit details
    Browse the repository at this point in the history

  8. pyk/kast/outer: typo in comment

    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    1636750 View commit details
    Browse the repository at this point in the history

  9. pyk/tests/integration/{simple-proofs.k,test_simple_proofs.py}: update… 

    … tests to working version
    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    76d33e9 View commit details
    Browse the repository at this point in the history

  10. pyk/konvert/_kast_to_kore: correctly handle conversion of variables i… 

    …n concrete/symbolic attribute too
    @ehildenb
    ehildenb committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    b90e65d View commit details
    Browse the repository at this point in the history

Commits on Nov 12, 2024

  1. pyk/tests/integration/konvert/test_simple_proofs: update tests

    @ehildenb
    ehildenb committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    1af260b View commit details
    Browse the repository at this point in the history

  2. pyk/tests/integration/proof/test_imp: update function argument names

    @ehildenb
    ehildenb committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    ff1d21f View commit details
    Browse the repository at this point in the history

  3. pyk/konvert/_kast_to_kore: working conversion of K functional rules t… 

    …o kore
    @ehildenb
    ehildenb committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    f394c77 View commit details
    Browse the repository at this point in the history

  4. pyk/reachability: support adding extra Kast modules to proof context

    @ehildenb
    ehildenb committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    610949c View commit details
    Browse the repository at this point in the history

Commits on Nov 13, 2024

  1. pyk/konvert/_kast_to_kore: make sure to sort attribute entries first

    @ehildenb
    ehildenb committed Nov 13, 2024
    Configuration menu
    Copy the full SHA
    cbdc23c View commit details
    Browse the repository at this point in the history