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

Solver result caching #1873

Merged
merged 53 commits into from
Jul 27, 2023
Merged

Solver result caching #1873

merged 53 commits into from
Jul 27, 2023

Commits on May 8, 2023

  1. quick and dirty solver caching

    @m-yac
    m-yac committed May 8, 2023
    Configuration menu
    Copy the full SHA
    bf22047 View commit details
    Browse the repository at this point in the history

  2. move files, fix cache loading

    @m-yac
    m-yac committed May 8, 2023
    Configuration menu
    Copy the full SHA
    e6a4513 View commit details
    Browse the repository at this point in the history

  3. add --cache command-line option

    @m-yac
    m-yac committed May 8, 2023
    Configuration menu
    Copy the full SHA
    d648970 View commit details
    Browse the repository at this point in the history

Commits on May 9, 2023

  1. save SolverStats when caching solver results

    @m-yac
    m-yac committed May 9, 2023
    Configuration menu
    Copy the full SHA
    92aee03 View commit details
    Browse the repository at this point in the history

  2. use strings as solver result cache keys since Terms have non-unique h… 

    …ashes
    @m-yac
    m-yac committed May 9, 2023
    Configuration menu
    Copy the full SHA
    70b9be0 View commit details
    Browse the repository at this point in the history

  3. save solver result cache on :q

    @m-yac
    m-yac committed May 9, 2023
    Configuration menu
    Copy the full SHA
    072cf1a View commit details
    Browse the repository at this point in the history

Commits on May 10, 2023

  1. use sha256 for solver result caching, save cache after each REPL command

    @m-yac
    m-yac committed May 10, 2023
    Configuration menu
    Copy the full SHA
    d870ea6 View commit details
    Browse the repository at this point in the history

  2. remove 'x' prefix from solver result cache files

    @m-yac
    m-yac committed May 10, 2023
    Configuration menu
    Copy the full SHA
    f05bc40 View commit details
    Browse the repository at this point in the history

  3. improve hash function for SolverCacheKey, reorganize SolverCache.hs

    @m-yac
    m-yac committed May 10, 2023
    Configuration menu
    Copy the full SHA
    cd5cc1b View commit details
    Browse the repository at this point in the history

  4. load and save cached results only when needed

    @m-yac
    m-yac committed May 10, 2023
    Configuration menu
    Copy the full SHA
    e5dcdda View commit details
    Browse the repository at this point in the history

  5. add print_solver_cache_stats

    @m-yac
    m-yac committed May 10, 2023
    Configuration menu
    Copy the full SHA
    63eed88 View commit details
    Browse the repository at this point in the history

Commits on May 11, 2023

  1. use prettyprinting functions for showing FiniteValues and FirstOrderV… 

    …alues
    @m-yac
    m-yac committed May 11, 2023
    Configuration menu
    Copy the full SHA
    9fb0c6d View commit details
    Browse the repository at this point in the history

Commits on May 16, 2023

  1. factor sequentToSATQuery out of SMT backends, cache counterexamples

    @m-yac
    m-yac committed May 16, 2023
    Configuration menu
    Copy the full SHA
    37be6ca View commit details
    Browse the repository at this point in the history

Commits on May 17, 2023

  1. anonymize local names in satQueryToSolverCacheKey

    @m-yac
    m-yac committed May 17, 2023
    Configuration menu
    Copy the full SHA
    7e264c5 View commit details
    Browse the repository at this point in the history

Commits on May 18, 2023

  1. make SolverCache an IORef in TopLevel so entries persist after failure

    @m-yac
    m-yac committed May 18, 2023
    Configuration menu
    Copy the full SHA
    3cc4d1e View commit details
    Browse the repository at this point in the history

Commits on May 19, 2023

  1. add documentation to SolverCache.hs

    @m-yac
    m-yac committed May 19, 2023
    Configuration menu
    Copy the full SHA
    084dd14 View commit details
    Browse the repository at this point in the history

Commits on May 20, 2023

  1. include solver backend versions in solver caching

    @m-yac
    m-yac committed May 20, 2023
    Configuration menu
    Copy the full SHA
    fcef4ec View commit details
    Browse the repository at this point in the history

Commits on May 23, 2023

  1. use LMDB for solver result caching

    @m-yac
    m-yac committed May 23, 2023
    Configuration menu
    Copy the full SHA
    e5ac59d View commit details
    Browse the repository at this point in the history

Commits on May 24, 2023

  1. use CI scripts from input-output-hk/haskell-lmdb

    @m-yac
    m-yac committed May 24, 2023
    Configuration menu
    Copy the full SHA
    7de326a View commit details
    Browse the repository at this point in the history

  2. remove cp of lmdb pkgconfig, add lib and include to PATH for Windows

    @m-yac
    m-yac committed May 24, 2023
    Configuration menu
    Copy the full SHA
    b3b46f8 View commit details
    Browse the repository at this point in the history

  3. cleanup, revert most of 9fb0c6d

    @m-yac
    m-yac committed May 24, 2023
    Configuration menu
    Copy the full SHA
    03eec2e View commit details
    Browse the repository at this point in the history

  4. get lmdb-simple working with GHC 9.2.7

    @m-yac
    m-yac committed May 24, 2023
    Configuration menu
    Copy the full SHA
    751f54d View commit details
    Browse the repository at this point in the history

  5. add clean_solver_cache command

    @m-yac
    m-yac committed May 24, 2023
    Configuration menu
    Copy the full SHA
    0719bda View commit details
    Browse the repository at this point in the history

  6. try to get LMDB on Windows working on CI

    @m-yac
    m-yac committed May 24, 2023
    Configuration menu
    Copy the full SHA
    dec00ff View commit details
    Browse the repository at this point in the history

Commits on Jun 20, 2023

  1. use Python LMDB bindings for solver caching (TODO docs)

    @m-yac
    m-yac committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    3a77eb8 View commit details
    Browse the repository at this point in the history

  2. quick clean up to solver caching code

    @m-yac
    m-yac committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    c877623 View commit details
    Browse the repository at this point in the history

  3. replace solver caching CLI option with an env variable

    @m-yac
    m-yac committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    d7ae967 View commit details
    Browse the repository at this point in the history

  4. add docs to solver caching code

    @m-yac
    m-yac committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    9eae671 View commit details
    Browse the repository at this point in the history

Commits on Jun 21, 2023

  1. add test for solver result caching

    @m-yac
    m-yac committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    c36cb0d View commit details
    Browse the repository at this point in the history

  2. expand tests for solver caching

    @m-yac
    m-yac committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    f173acb View commit details
    Browse the repository at this point in the history

  3. actually install lmdb on the CI for solver caching tests

    @m-yac
    m-yac committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    bfb1b79 View commit details
    Browse the repository at this point in the history

Commits on Jun 22, 2023

  1. set -e in test_solver_cache

    @m-yac
    m-yac committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    2354bb2 View commit details
    Browse the repository at this point in the history

  2. WIP testing saving LMDB caches on CI

    @m-yac
    m-yac committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    16cfe0e View commit details
    Browse the repository at this point in the history

Commits on Jun 27, 2023

  1. WIP more CI debugging

    @m-yac
    m-yac committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    897f8ff View commit details
    Browse the repository at this point in the history

  2. remove hex-text dependency, confirm no exns with units in LMDBOptData… 

    …base
    @m-yac
    m-yac committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    c040ab5 View commit details
    Browse the repository at this point in the history

  3. get SBV version through cabal VERSION macro, not freeze file

    @m-yac
    m-yac committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    c68801d View commit details
    Browse the repository at this point in the history

  4. fix style issues / typos found by @RyanGlScott

    @m-yac
    m-yac committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    964219c View commit details
    Browse the repository at this point in the history

  5. add forgotten base case to decodeHex

    @m-yac
    m-yac committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    b3575ea View commit details
    Browse the repository at this point in the history

  6. pip install lmdb in test_solver_cache/test.sh

    @m-yac
    m-yac committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    6a5ec67 View commit details
    Browse the repository at this point in the history

Commits on Jun 28, 2023

  1. improve test_solver_cache_stats args, clean up debugging code, add docs

    @m-yac
    m-yac committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    0e2efb2 View commit details
    Browse the repository at this point in the history

  2. update the SAW manual with information about solver caching

    @m-yac
    m-yac committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    bbdfdf0 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2023

  1. fix/improve getSolverVersion for yices and others

    @m-yac
    m-yac committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    7721cfb View commit details
    Browse the repository at this point in the history

Commits on Jul 21, 2023

  1. solver caching: use lmdb-simple, make env var lazy, save timestamps

    @m-yac
    m-yac committed Jul 21, 2023
    Configuration menu
    Copy the full SHA
    fa146c8 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2023

  1. move python interface for SAW solver caches to saw-remote-api

    @m-yac
    m-yac committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    c426c71 View commit details
    Browse the repository at this point in the history

  2. update docs for solver caching

    @m-yac
    m-yac committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    aea7c08 View commit details
    Browse the repository at this point in the history

  3. update solver cache tests, fix but in clean_solver_cache

    @m-yac
    m-yac committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    b29790c View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into solver-caching

    @m-yac
    m-yac committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    9bd0bd3 View commit details
    Browse the repository at this point in the history

  5. update solver cache testing on CI

    @m-yac
    m-yac committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    5f2f2f9 View commit details
    Browse the repository at this point in the history

  6. improve layout of docstrings for solver_cache_stats commands

    @m-yac
    m-yac committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    c28e340 View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2023

  1. make SolverCacheOp a datatype for clarity

    @m-yac
    m-yac committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    bc446cf View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into solver-caching

    @m-yac
    m-yac committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    2fde0df View commit details
    Browse the repository at this point in the history

  3. resolve some comments from @RyanGlScott

    @m-yac
    m-yac committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    9c5c394 View commit details
    Browse the repository at this point in the history

  4. move JSON instances and add associated docs to FiniteValue.hs

    @m-yac
    m-yac committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    a960c36 View commit details
    Browse the repository at this point in the history