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.

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

Do not use vectors indexed by Pterms' ids in LASolver #500

Open
wants to merge 4 commits into
base: master
Choose a base branch
from

Commits on May 25, 2022

  1. LASolver: Avoid vectors with large gaps

    When LAVarMapper is storing mapping from PTerms to LATerms as vectors
    with TermId as index, this creates possibly huge vectors with just a
    small number of entries filled. This is not a problem for single-use
    instances, but in applications where number of terms in Logic is growing
    constantly are a solver is queries repeatedly, the initialization of
    LASolver due to allocation of large vectors starts to be noticeable.
    
    For now we use standard hashmap as a replacement. It seems that some
    kind of flat map, which additioanlly does not need to support deletion
    could be even better.
    Martin Blicha committed May 25, 2022
    Configuration menu
    Copy the full SHA
    2ca2142 View commit details
    Browse the repository at this point in the history
  2. Remove redundant method

    Martin Blicha committed May 25, 2022
    Configuration menu
    Copy the full SHA
    7b8f262 View commit details
    Browse the repository at this point in the history
  3. LASolver: Use map instead of sparse vector to remember atom-to-bounds…

    … mapping
    Martin Blicha committed May 25, 2022
    Configuration menu
    Copy the full SHA
    b0f3a3b View commit details
    Browse the repository at this point in the history
  4. LASolver: Use mtl's Map instead of std::unoredered_map

    Martin Blicha committed May 25, 2022
    Configuration menu
    Copy the full SHA
    f5834c2 View commit details
    Browse the repository at this point in the history