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

Induction and first-order assertions #1724

Closed
wants to merge 9 commits into from
Closed

Induction and first-order assertions #1724

wants to merge 9 commits into from

Commits on Aug 9, 2022

  1. Add some direct SAWCore proofs of facts leading to the complete 

    induction principle for natural numbers, and for bitvectors.

This adds no additional axioms over those alreay present in the
system.
    @robdockins
    robdockins committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    c06915b View commit details
    Browse the repository at this point in the history

Commits on Aug 12, 2022

  1. First cut at building bitvector induction schemas

    @robdockins
    robdockins committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    d52fe4b View commit details
    Browse the repository at this point in the history

  2. Begin adding infrastructure to allow universally-quantified 

    assertions to be passed to solvers.
    @robdockins
    robdockins committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    95ab709 View commit details
    Browse the repository at this point in the history

  3. Add helpers for computing multiple and or or applications.

    @robdockins
    robdockins committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    043c91a View commit details
    Browse the repository at this point in the history

  4. Further work on universal assertions.

    @robdockins
    robdockins committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    f7052e8 View commit details
    Browse the repository at this point in the history

  5. whitespace

    @robdockins
    robdockins committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    9ca6b13 View commit details
    Browse the repository at this point in the history

  6. Add a test case for asserting universally-quantified statements. 

    Fixes #1037
    @robdockins
    robdockins committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    a2ffe1e View commit details
    Browse the repository at this point in the history

  7. Comment-out some code to squash a warning

    @robdockins
    robdockins committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    956060c View commit details
    Browse the repository at this point in the history

  8. squash a warning

    @robdockins
    robdockins committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    5772173 View commit details
    Browse the repository at this point in the history