Fixes #11
Open
Fixes #11
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Move vector initialization 2 loops out, to reduce the number of re-alloactions.
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.
The tmp dir variable has been read from $3, while $2 was the actual aim.
In the old version, the wrong variable has been used as index value, leading to out of bound errors.
If there are no candidate literals to compute a score for, stop the computation, and skip.
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.
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.
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.
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.
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.
When we know a level does not have clauses to share, do not lock the level, but instead skip the level right away.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a series of commits that fix certain wrong behaviour that has been encountered while playing with the solver.
Commit "splitting: handle no-split case" needs some attention, using lit_Undef as default value might come with side effects.