summaryrefslogtreecommitdiff
path: root/src/prop/minisat
AgeCommit message (Expand)Author
2011-10-03user push/pop support in minisat and simplification; also bindings workMorgan Deters
2011-09-30more push/pop infrastructure, some SAT stuffMorgan Deters
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop a...Morgan Deters
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-09-02* Changing pre-registration to be context dependent -- it is called from the ...Dejan Jovanović
2011-08-30Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK wil...Dejan Jovanović
2011-08-17new implementation of lemmas on demandDejan Jovanović
2011-07-11merge from symmetry branchMorgan Deters
2011-07-10changing the sat solver remove clauses constantsDejan Jovanović
2011-07-06Fixing two bugs:Dejan Jovanović
2011-04-14reverting back the minisat code and adding a simpler one that shouldn't chang...Dejan Jovanović
2011-04-14fixing an uninitialized literal variableDejan Jovanović
2011-04-13adding support for unit conflicts in minisat...Dejan Jovanović
2011-04-10merge from replay branchMorgan Deters
2011-04-09changing the sat solver to assert propagated literals back to the theoriesDejan Jovanović
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
2011-03-30Add Valuation::getSatValue() so that theories can access the currentMorgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2011-03-15real fix for bug 245, previous one was faultyDejan Jovanović
2011-03-15fix for bug 254, lemmas were propagating at lower levels, and the conflict cl...Dejan Jovanović
2011-03-03fixing a type that caused the segfaults in the regressionsDejan Jovanović
2011-03-02fixing the big with lemma reallocation in minisat garbage collectionDejan Jovanović
2011-02-26Commit to fix bug 241 (improper "using namespace std" in a header). This cau...Morgan Deters
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-15Changes to Solver and PropEngine to support lemmasOnDemand during solve but n...Tim King
2010-11-12Some bug fixes in the SAT for lemmas, and an experiment with a more complete ...Dejan Jovanović
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-10-27"make dist" fixes; a distribution tarball can now build and pass tests. "make...Morgan Deters
2010-08-20updating the minisat restart parameters after running some experimentsDejan Jovanović
2010-08-16Fixing failures in minisatDejan Jovanović
2010-08-15(no commit message)Dejan Jovanović
2010-08-13renaming minisat .C to .cc Dejan Jovanović
2010-08-13Adding the changes to the original copyDejan Jovanović
2010-08-13Importing MiniSat2 070721 into trunkChristopher L. Conway
2010-08-13Removing newer version of MiniSat for Dejan's preferred importChristopher L. Conway
2010-08-13Importing MiniSat2 2.2.0 into trunkChristopher L. Conway
2010-08-13Removing old version of MiniSat for proper vendor importChristopher L. Conway
2010-07-03With this commit come a number of changes to build system to supportMorgan Deters
2010-06-29Merging the unate-propagator branch into the trunk. This is a big update so ...Tim King
2010-06-15fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)Morgan Deters
2010-06-15remove warnings about unknown #pragma GCC diagnostic on older compilersMorgan Deters
2010-05-25Some initial changes to allow for lemmas on demand. Dejan Jovanović
2010-04-15Adding info in the minisat READMEDejan Jovanović
2010-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
2010-04-01PARSER STUFF:Morgan Deters
2010-03-30Removing unnecessary .gitignoresChristopher L. Conway
2010-03-30Merging from branches/antlr3 (r246:354)Christopher L. Conway
2010-03-12* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,Morgan Deters
2010-03-11Fix for the main bug that was bugging me -- Bug 49. The assertions queue in t...Dejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback