summaryrefslogtreecommitdiff
path: root/src/prop/bvminisat
AgeCommit message (Expand)Author
2016-09-01Relaxing the throw specifiers for the destructors for Node, TypeNode, the con...Tim King
2016-05-24Merged cryptominisat from experimental branch.Liana Hadarean
2016-02-24Unifying the definitions of ClauseId to a single source of truth.Tim King
2016-01-28Adding listeners to Options.Tim King
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
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
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2014-11-18All Minisat solve calls now return lbool (fixes bug 599)lianah
2014-11-17Resource-limiting work.Liana Hadarean
2014-11-07Remove some dead code.Morgan Deters
2014-10-06Fix a resource limiting issue where interruption didn't occur promptly. Than...Morgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-04Better support for resource-limiting when there aren't any actual conflicts.Morgan Deters
2014-07-10Merge remote-tracking branch 'origin/master' into segfaultfixKshitij Bansal
2014-07-04initialize variablesKshitij Bansal
2014-06-21Fix compiler warnings in BV-related code (unused vars mostly).Morgan Deters
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-11-27Fix for compile error when using gcc 4.7 with -std=gnu++11. Thanks to Martin...Morgan Deters
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-04-30added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExt...lianah
2013-04-30added bvule, bvsle operator elimination rulesl; added bvurem lemma generationlianah
2013-04-03* changing the bitblast-eager to bitblast on pre-registerDejan Jovanović
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
2013-02-16Some cleanup and copyright updatingMorgan Deters
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2012-12-06* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issuesMorgan Deters
2012-12-06* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issuesMorgan Deters
2012-10-03added support for interrupting TheoryBVLiana Hadarean
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-08-06removing the sat solver inmterface from being publicDejan Jovanović
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-27break dependence on zlib-dev for nowMorgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback