projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
This is a merge from the "theoryfixes+cdattrhash" branch. The changes
[cvc5.git] / src / theory / theory.h
2011-03-25 Morgan DetersThis is a merge from the "theoryfixes+cdattrhash" branc... blob | commitdiff | raw
2011-03-08 Morgan DetersClean up Theory base class as per code review bug ... blob | commitdiff | raw | diff to current
2011-02-27 Tim King- Adds a path for Theory to be passed a reference to... blob | commitdiff | raw | diff to current
2011-02-26 Morgan DetersMerge from theory-break-dependences branch to break... blob | commitdiff | raw | diff to current
2011-01-05 Dejan JovanovićCommit for the theory engine and rewriter changes.... blob | commitdiff | raw | diff to current
2010-11-24 Dejan JovanovićChangin the get() semantics to a CDQeue-sque semantics. blob | commitdiff | raw | diff to current
2010-11-19 Morgan DetersMerge from ufprop branch, including: blob | commitdiff | raw | diff to current
2010-11-16 Tim KingAdded Theory::presolve(). blob | commitdiff | raw | diff to current
2010-10-09 Morgan DetersModel generation for arith, boolean, and uf theories via blob | commitdiff | raw | diff to current
2010-10-03 Morgan Detersfile header documentation regenerated with contributors... blob | commitdiff | raw | diff to current
2010-08-19 Morgan DetersUF theory bug fixes, code cleanup, and extra debugging... blob | commitdiff | raw | diff to current
2010-07-07 Clark BarrettShared term manager tested and working blob | commitdiff | raw | diff to current
2010-07-07 Clark BarrettAdded shared term manager. Basic mechanism for identif... blob | commitdiff | raw | diff to current
2010-07-06 Clark BarrettMoved registration to theory engine blob | commitdiff | raw | diff to current
2010-07-04 Morgan DetersWith "-d extra-checking", rewrites are now checked... blob | commitdiff | raw | diff to current
2010-07-02 Morgan Deters* Added white-box TheoryEngine test that tests the... blob | commitdiff | raw | diff to current
2010-06-30 Morgan Deters* theory "tree" rewriting implemented and works blob | commitdiff | raw | diff to current
2010-06-29 Tim KingMerging the unate-propagator branch into the trunk... blob | commitdiff | raw | diff to current
2010-06-15 Tim KingI made a documentation change to get() to make explicit... blob | commitdiff | raw | diff to current
2010-06-04 Morgan Deters** Don't fear the files-changed list, almost all change... blob | commitdiff | raw | diff to current
2010-04-04 Morgan Deters* Node::isAtomic() now looks at an "atomic" attribute... blob | commitdiff | raw | diff to current
2010-04-01 Morgan DetersPARSER STUFF: blob | commitdiff | raw | diff to current
2010-03-30 Morgan DetersHighlights of this commit are: blob | commitdiff | raw | diff to current
2010-03-12 Morgan Deters* Added shutdown() functions to SmtEngine, TheoryEngine... blob | commitdiff | raw | diff to current
2010-03-11 Morgan Detersnaive rewriting to fix minisat invariant; rewrite ... blob | commitdiff | raw | diff to current
2010-03-11 Dejan JovanovićFix for the main bug that was bugging me -- Bug 49... blob | commitdiff | raw | diff to current
2010-03-08 Dejan Jovanovićadding simple-uf to the regressions, and the code that... blob | commitdiff | raw | diff to current
2010-02-28 Tim KingTheoryUFWhite is passing. I fixed 2 errors. Unfortunat... blob | commitdiff | raw | diff to current
2010-02-26 Morgan Deters* test/unit/context/context_black.h: Test CDList<>... blob | commitdiff | raw | diff to current
2010-02-26 Tim KingTheoryUFWhite tests are added. There are also accompany... blob | commitdiff | raw | diff to current
2010-02-25 Morgan Deters* src/expr/node.h: add a copy constructor. Apparently... blob | commitdiff | raw | diff to current
2010-02-24 Tim KingCommitting small changes to attribute, and theory to... blob | commitdiff | raw | diff to current
2010-02-22 Morgan Deters* configure.ac: Remove doc/ from search path for Makefi... blob | commitdiff | raw | diff to current
2010-02-22 Morgan DetersRe-committing revision 232 properly: blob | commitdiff | raw | diff to current
2010-02-22 Morgan Detersundoing improperly-committed revision 232; will re... blob | commitdiff | raw | diff to current
2010-02-22 Cesare Tinelli* Add virtual destructors to CnfStream, Theory, OutputC... blob | commitdiff | raw | diff to current
2010-02-17 Tim KingInitial draft of TheoryUF. Should compile without probl... blob | commitdiff | raw | diff to current
2010-02-10 Morgan Detersnote on setup(); for discussion at 2010.02.11 meeting blob | commitdiff | raw | diff to current
2010-02-04 Morgan Detersminor interface changes to TheoryEngine/Theory after... blob | commitdiff | raw | diff to current
2010-02-04 Morgan Detersremove -*- c++ -*- emacs tag from source files (it... blob | commitdiff | raw | diff to current
2010-02-04 Morgan DetersAdded theory output channel interfaces and "Interrupted... blob | commitdiff | raw | diff to current
2010-01-29 Morgan Detersfixed CNF conversion, and more modular; CNF conversion... blob | commitdiff | raw | diff to current
2010-01-19 Morgan Detersminor changes to Theory blob | commitdiff | raw | diff to current
2009-12-17 Morgan Detersupdate-copyright.pl now retrieves and incorporates... blob | commitdiff | raw | diff to current
2009-12-10 Dejan Jovanovićkilling expr into node... blob | commitdiff | raw | diff to current
2009-11-24 Morgan Detersconfigure option adjustments as per 11/24 meeting;... blob | commitdiff | raw | diff to current
2009-11-23 Morgan Detersfixups, file comments blob | commitdiff | raw | diff to current
2009-11-19 Morgan Deterstesting framework, configure fixes, incorporations... blob | commitdiff | raw | diff to current
2009-11-17 Morgan Detersfrom meeting blob | commitdiff | raw | diff to current