projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fefdd35) | patch
Cleanup Cryptominisat SAT wrapper. (#1652)
authorMathias Preiner <mathias.preiner@gmail.com>
Fri, 9 Mar 2018 02:42:03 +0000 (18:42 -0800)
committerGitHub <noreply@github.com>
Fri, 9 Mar 2018 02:42:03 +0000 (18:42 -0800)
commit4c64f2388a5dca50ecbd0610f9dcb13324345b94
tree7f4c3218a3dcb9fa0012465c2a027e0a47b01962tree
parentfefdd3589804d989e5be641aa8daaaa82369e18ccommit | diff
Cleanup Cryptominisat SAT wrapper. (#1652)

Cryptominisat has name conflicts with the other Minisat implementations since
the Minisat implementations export var_Undef, l_True, ... as macro whereas
Cryptominisat uses static const. In order to avoid these conflicts we
forward declare CMSat::SATSolver and include the cryptominisat header only
in cryptominisat.cpp.

Further, the helper functions are moved into an anonymous namespace in the .cpp file and functions that were not used are removed.
contrib/get-cryptominisat4 diff | blob | history
src/prop/cryptominisat.cpp diff | blob | history
src/prop/cryptominisat.h diff | blob | history
src/prop/sat_solver_factory.cpp diff | blob | history