coverity: add to travis #3
Closed
Conversation
This file contains hidden or 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
Moved all source files to a "minisat" subdirectory and changed includes to take this into account. NOTE: all usages of MiniSat will also have to adapt to this new directory layout.
Mainly fixes a problem with builds that needs multiple modes (release, dynamic, etc). The current solution is ugly (cut'n'paste), but I haven't found something better that works yet.
Thanks to Michael Tautschnig <mt@debian.org> suggesting the fixes.
Note that this changes the interface for setting variable polarities.
Added a -strict flag that checks correctness of "p cnf" line.
…nisat::memUsedPeak() for OSX, BSD and other non-Linux platforms
…which evaluates to a string), in order to avoid definition of user-defined trigraphs.
When the rule for dynamic library is run in parallel (using make -jX), it can overwrite one file multiple times resulting in errors like: build/dynamic/lib/libminisat.so: file not recognized: File format not recognized Fix it by splitting and making an explicit dependency in Makefile. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
When compiling with more recent compilers, the format string and PRIu64 have to be separated, otherwise, a warning is produced. Hence, separate them.
For now, make sure the relevant solver targets can be compiled with a recent compiler.
By adding a starexec template and a script to build the starexec package, future submissions of Minisat to the SAT competition will be simpler.
While Minisat prints the output state without the 's ' prefix, and prints models without the 'v ' prefix, the SAT competition, and related events require those prefixes. Furthermore, Minisat does not print the model to the screen by default. Finally, any other data that is printed by Minisat is not prefixed by a 'c ', so that output scanners might be confused. To make the output of the solver ready for competitions, add the 's ' and 'v ' prefixes, and 'c ' prefix to the messages that are printed independently of the set verbosity.
The original variant of Minisat prints the model only to the output file, but did not print it to screen. For competitions, the model has to be printed as well, hence, it was added to the previous commit. To be able to restore the old behavior, add a CLI parameter "-model", that controls whether the values of the model are printed. When specifying '-no-model' as a parameter, no model is printed.
This commit adds printing proofs to a file. To allow printing, the API of the solver is extended by three functions that open a proof file, extend the proof by adding or deleting a clause, or finalize the proof and close the file again. For the simplifying solver, an operation mode flag is introduced, which indicates that the solver currently parses the input. During operation, the solver only uses the extendProof method. This allows to easily adapt the format in the future. This commit is based on the patch by Marijn Heule that modified an older version of Minisat (v2.2.0) to comply with the SAT competition rules: http://www.satcompetition.org/2013/files/MinisatHack.patch In this commit, only the proof generation is implemented. And furthermore a bug in the addClause method is fixed, recognizing tautologies correctly.
To print proofs to files, the parameter '-proof' has been added. In case that parameter is specified, the specified value is used as filename and opened for writing. In the simplifying solver, the operation of parsing had to be indicated as well, to process the proof information correctly.
As the SAT competition verifies the output, and checks for certain prefixes, make sure everything that is not a solution or truth value is treated as comment.
conp-solutions
pushed a commit
that referenced
this pull request
Jun 14, 2020
* Minimal LSIDS * Bump for non-VSIDS section, Decaying * bump lit scores during cancelUntil * Creating lit_decay
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.
Run Coverity on changes of repository.