summaryrefslogtreecommitdiff
path: root/src/prop
AgeCommit message (Expand)Author
2010-07-04Considerably simplified the way output streams are used. This commitMorgan Deters
2010-07-04make dist && make distcheck functional, other fixesMorgan Deters
2010-07-03With this commit come a number of changes to build system to supportMorgan Deters
2010-07-02re-generated comment headers of source filesMorgan Deters
2010-06-30* theory "tree" rewriting implemented and worksMorgan 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-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-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-06-01In order for splitting on demand to be able to retract clauses every translat...Dejan Jovanović
2010-05-28Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer ...Tim King
2010-05-27Remove isAtomic() as per 4/27/2010 meeting. Add comments about its potential...Morgan Deters
2010-05-27Preregistration has been turned on. Highly experimental eager splitting suppo...Tim King
2010-05-25Some initial changes to allow for lemmas on demand. Dejan Jovanović
2010-05-21Small fixes to TheoryArith. Added a hack to make Integers a subtype of Real....Tim King
2010-05-14Adding debugging code in PropEngine/CnfStreamChristopher L. Conway
2010-05-14Adding rudimentary ITE handling in CnfStreamChristopher L. Conway
2010-05-14Virtualizing interface between CnfStream and SatSolverChristopher L. Conway
2010-05-13Minor refactorings to PropEngine, SatSolverChristopher L. Conway
2010-05-13Minor refactorings and corrections to commentsChristopher L. Conway
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-01reran update-copyright.pl to get new contributors and add new header comments...Morgan 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-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-11Boolean variables were marked as theory literals by mistake. Fixed, should gi...Dejan Jovanović
2010-03-11Fix for the main bug that was bugging me -- Bug 49. The assertions queue in t...Dejan Jovanović
2010-03-09(no commit message)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-05* public/private code untangled (smt/smt_engine.h no longer #includesMorgan Deters
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-03-02* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"Morgan Deters
2010-02-26* test/unit/context/context_black.h: Test CDList<>. In particular,Morgan Deters
2010-02-25* src/expr/node.h: add a copy constructor. Apparently GCC doesn'tMorgan Deters
2010-02-22Merging from branch branches/Liana r241Dejan Jovanović
2010-02-22* configure.ac: Remove doc/ from search path for Makefile.amsMorgan Deters
2010-02-22Re-committing revision 232 properly:Morgan Deters
2010-02-22undoing improperly-committed revision 232; will re-commit to get "svn blame" ...Morgan Deters
2010-02-22* Add virtual destructors to CnfStream, Theory, OutputChannel, andCesare Tinelli
2010-02-19* Attribute infrastructure -- static design. Documentation is coming.Morgan Deters
2010-02-13simplification minisat Dejan Jovanović
2010-02-13Improvements to CNF conversion when already in CNFDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback