summaryrefslogtreecommitdiff
path: root/src/prop/bvminisat/core
AgeCommit message (Expand)Author
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2018-12-03Bit vector proof superclass (#2599)Alex Ozdemir
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-10-01Fix compiler warnings. (#2555)Aina Niemetz
2018-09-13Fix #include for minisat headers in bvminisat. (#2463)Mathias Preiner
2018-07-30Fix several spelling errors (#2231)FabianWolff
2018-05-23Remove ProofProxy (#1965)Andres Noetzli
2018-04-03[BVMiniSat] Avoid duplicates in conflicts (#1745)Andres Noetzli
2018-01-15Removing more miscellaneous throw specifiers. (#1509)Tim King
2017-09-25Initializing BVMinisat Solver::notify to nullptr. (#1132)Tim King
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2016-04-20update from the masterPaulMeng
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-10-26This fixes a one definition rule violation for reduceDB_lt in Solver.cc in mi...Tim King
2015-05-29changed resource step options to unsignedlianah
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2014-11-18All Minisat solve calls now return lbool (fixes bug 599)lianah
2014-11-17Resource-limiting work.Liana Hadarean
2014-07-04initialize variablesKshitij Bansal
2014-06-13fixed BVMinisat bug due to not clearing seen properlylianah
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-03-19Appease compilers from latest XCode release (v5.1).Morgan Deters
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2012-10-03added support for interrupting TheoryBVLiana Hadarean
2012-07-31Options merge. This commit:Morgan Deters
2012-06-14fixing the problems with the bvminisat. there was a case when things would ge...Dejan Jovanović
2012-06-11fixing bitvector bugsDejan Jovanović
2012-05-15several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify a...Liana Hadarean
2012-05-13fixing build warningsDejan Jovanović
2012-05-09* simplifying equality engine interfaceDejan Jovanović
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
2012-05-03Some cleanup starting off from trying to understand the sharing code. Changes...Dejan Jovanović
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-04some settings in bvminisatDejan Jovanović
2012-04-04changed BVMinisat options to use cc_min=0 in propagate only calls and cc_min=...Liana Hadarean
2012-04-04changed ccmin_mode in BvMinisatLiana Hadarean
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
2012-03-22Merged updated version of the bitvector theory:Liana Hadarean
2012-02-29This should fix the debian build fails:Liana Hadarean
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback