summaryrefslogtreecommitdiff
path: root/src/prop/sat.h
AgeCommit message (Expand)Author
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02* Changing pre-registration to be context dependent -- it is called from the ...Dejan Jovanović
2011-08-17new implementation of lemmas on demandDejan Jovanović
2011-04-10merge from replay branchMorgan Deters
2011-04-05Added options for setting the random decision frequency and random seed for t...Tim King
2011-04-01documentation fixMorgan Deters
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
2011-03-31Fixes to Valuation.Tim King
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-10-22Merging main/getopt.cpp, main/usage.h, and smt/options.h inChristopher L. Conway
2010-10-21* Option --no-type-checking now disables type checks in SmtEngineChristopher L. Conway
2010-10-10additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp...Morgan Deters
2010-10-09Model generation for arith, boolean, and uf theories viaMorgan Deters
2010-10-03file header documentation regenerated with contributors names; no code modifi...Morgan Deters
2010-09-21fix statistics-registry-related memory leaksMorgan Deters
2010-08-20updating the minisat restart parameters after running some experimentsDejan Jovanović
2010-08-15(no commit message)Dejan Jovanović
2010-07-07Added shared term manager. Basic mechanism for identifying shared terms isClark Barrett
2010-07-04Considerably simplified the way output streams are used. This commitMorgan Deters
2010-07-02re-generated comment headers of source filesMorgan Deters
2010-06-29Merging the unate-propagator branch into the trunk. This is a big update so ...Tim King
2010-06-18Merging the statistics branch into the main trunk. I'll go over how to use th...Tim King
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-05-25Some initial changes to allow for lemmas on demand. Dejan Jovanović
2010-05-14Adding debugging code in PropEngine/CnfStreamChristopher L. Conway
2010-05-14Virtualizing interface between CnfStream and SatSolverChristopher L. Conway
2010-05-13Minor refactorings to PropEngine, SatSolverChristopher L. Conway
2010-04-01reran update-copyright.pl to get new contributors and add new header comments...Morgan Deters
2010-04-01PARSER STUFF:Morgan Deters
2010-03-25Adding comments to NodeManagerChristopher L. Conway
2010-03-12Fixing unnecessary construction of NOT nodes when generating conflict clause...Dejan Jovanović
2010-03-12* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,Morgan Deters
2010-03-11Changing const TNode& to TNode in the CNF conversion + a new small benchmark ...Dejan Jovanović
2010-03-11Fix for the main bug that was bugging me -- Bug 49. The assertions queue in t...Dejan Jovanović
2010-03-08adding simple-uf to the regressions, and the code that apparently solves itDejan Jovanović
2010-03-08some more sat stuff for tim: assertions now go to theory_uf Dejan Jovanović
2010-03-04Adding phase-caching to minisat. Dejan Jovanović
2010-03-03Some SAT stuff, not doing anything special yet, just to keep it in sync.Dejan Jovanović
2010-02-26* test/unit/context/context_black.h: Test CDList<>. In particular,Morgan Deters
2010-02-22* configure.ac: Remove doc/ from search path for Makefile.amsMorgan Deters
2010-02-13simplification minisat Dejan Jovanović
2010-02-09Changes to the CNF conversion and the SAT solver. All regression pass now, an...Dejan Jovanović
2010-02-04beautification of the prop engineDejan Jovanović
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing...Morgan Deters
2010-02-04minor fix for update-copyright.pl; ran update-copyright.pl on all sources; re...Morgan Deters
2009-12-17update-copyright.pl now retrieves and incorporates author information from re...Morgan Deters
2009-11-19testing framework, configure fixes, incorporations from meeting, continued workMorgan Deters
2009-11-17from meetingMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback