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

Fixes #11

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

Fixes #11

wants to merge 13 commits into from

Commits on Mar 6, 2020

  1. pcasso: try to avoid local data structures 

    Move vector initialization 2 loops out, to reduce the number of
re-alloactions.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    82e81e0 View commit details
    Browse the repository at this point in the history

  2. pcasso: get learnts_indeces right 

    When using an index to point into the learnts vector, make sure the items
in that vector are valid, or in release mode are dropped to not crash the
solver. This was found when using LCM which modified the learnts vector.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    275cf18 View commit details
    Browse the repository at this point in the history

  3. pcasso.sh: actually read tmp dir 

    The tmp dir variable has been read from $3, while $2 was the actual aim.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    96359f9 View commit details
    Browse the repository at this point in the history

  4. splitting: use var based index 

    In the old version, the wrong variable has been used as index value,
leading to out of bound errors.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    bc4d5af View commit details
    Browse the repository at this point in the history

  5. splitting: only compute score for candidates 

    If there are no candidate literals to compute a score for, stop the
computation, and skip.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    797ae6a View commit details
    Browse the repository at this point in the history

  6. splitting: handle no-split case 

    The split variable next has to be initialized, such that in case of
failures during computing the candidates, e.g. due to too small formulas,
there lit_Undef value can still be returned.

Consequently, make sure nobody consumes lit_Undef as an index.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    892cf06 View commit details
    Browse the repository at this point in the history

  7. master: allow getting stuck more often 

    As getting stuck might be due to a race condition, allow the solver to
see this condition more often before actually aborting the search. On the
other hand, make sure we assert before exit, so that debugging would be
doable, and the problem can be identified during fuzzing.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    10133b0 View commit details
    Browse the repository at this point in the history

  8. master: do not blindly set to unknown 

    When multiple slaves work on the same node, make sure they do not overwrite
the state of each other. Only set a state to unknown, if the node actually
has an unknown state.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    1c1cbc3 View commit details
    Browse the repository at this point in the history

  9. master: always write unsat result 

    Currently, the stopUnsatChilds option had to be set to write the unsat
state for a node. However, the state should always be written. Hence, the
check for the option is moved closer to actually running the related
algorithm.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    3abccb4 View commit details
    Browse the repository at this point in the history

  10. pcasso: clear clauses to share before reduceDB 

    In the reduceDB, new clauses are added to the clauses to be shared, but
no clauses are removed. This way, faulty pointers might be used, as the
clauses that are shared might become invalid, or wrong indexes are used.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    a21fc34 View commit details
    Browse the repository at this point in the history

  11. levelpool: inisist on more restrictions

    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    20c2e54 View commit details
    Browse the repository at this point in the history

  12. solverpt: do not share eagerly 

    When we know a level does not have clauses to share, do not lock the level,
but instead skip the level right away.
    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    b6262a0 View commit details
    Browse the repository at this point in the history

  13. solverpt: assertions and volatile

    @conp-solutions
    conp-solutions committed Mar 6, 2020
    Configuration menu
    Copy the full SHA
    b05be71 View commit details
    Browse the repository at this point in the history