summaryrefslogtreecommitdiff
path: root/src/prop/sat_solver_factory.cpp
AgeCommit message (Collapse)Author
2021-06-21Make CaDiCaL a required dependency. (#6761)Mathias Preiner
Since the new BV solver is enabled by default and uses CaDiCaL (and optionally CryptoMiniSat) we make CaDiCaL a required dependency.
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
This renames everything but GitHub links and build system related macros. Switching the build system to cvc5 will be the last step in the renaming process.
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
This PR refactors how we collect statistics. It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic. It also extends the C++ API to obtain and inspect the statistics. To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2020-12-14[proof-new] Updating interfaces between prop engine and minisat (#5664)Haniel Barbosa
This is in preparation to make the prop engine proof producing. This PR also renames "DPLLSatSolverInterface" to the more appropriate name "CDCLTSatSolverInterface". Note that most of the diff is due to formatting of the previously super ad-hoc formatting of the minisat code.
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-06-16Update copyright headers.Aina Niemetz
2020-05-22CaDiCaL: Clean up initialization on creation. (#4516)Aina Niemetz
2020-05-22Cryptominisat: Clean up initialization on creation. (#4515)Aina Niemetz
2020-05-22Add support for SAT solver Kissat. (#4514)Aina Niemetz
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-03-26Update copyright headers.Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-20Add support for CaDiCaL as eager BV SAT solver. (#1675)Mathias Preiner
2018-03-08Cleanup Cryptominisat SAT wrapper. (#1652)Mathias Preiner
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.
2018-02-07Cleanup Cryptominisat header. (#1561)Mathias Preiner
Clang formatted sat_solver_factor.cpp
2017-07-07Update copyright headers.Mathias Preiner
2016-05-24Merged cryptominisat from experimental branch.Liana Hadarean
2016-04-03Updating the copyright headers and scripts.Tim King
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit. - Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor. - The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit. - The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope. - Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead. - The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h. - Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added. - Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang. - Most of the really confusing ifdef's in util/statistics_registry.h are gone.
2014-11-07Remove some dead code.Morgan Deters
2014-11-07Fix a memory leak in SatSolverRegistry (re: bug #594).Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-06-10Merging CAV14 paper bit-vector work.lianah
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ↵Morgan Deters
\file tags corrected, copyright added to files that had it missing, etc. I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
* modified BVMinisat to work incrementally * added more bv regressions
2012-03-29Fixes a linking problem with the new SatSolverConstructor on Mac.Tim King
2012-03-28Some renaming and refactoring in SATDejan Jovanović
2012-03-26Global registry of SAT solvers, where they are registered at compile time. ↵Dejan Jovanović
The available SAT solvers can be seen with the --show-sat-solvers option.
2012-03-26More cleaning up.Dejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback