git.libre-soc.org Git - cvc5.git/history - src/theory/theory

[cvc5.git] / src / theory / theory_engine.h

2010-06-29	Tim King	Merging the unate-propagator branch into the trunk...	blob \| commitdiff \| raw
2010-06-24	Tim King	Added post_mortem.py a statistics collector for user...	blob \| commitdiff \| raw \| diff to current
2010-06-18	Tim King	Merging the statistics branch into the main trunk....	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-05-28	Tim King	A few changes to the organization of TheoryEngine rewri...	blob \| commitdiff \| raw \| diff to current
2010-05-28	Tim King	Moving the ITE removal from CnfStream to TheoryEngine...	blob \| commitdiff \| raw \| diff to current
2010-05-27	Tim King	Preregistration has been turned on. Highly experimental...	blob \| commitdiff \| raw \| diff to current
2010-05-25	Dejan Jovanović	Some initial changes to allow for lemmas on demand.	blob \| commitdiff \| raw \| diff to current
2010-05-20	Tim King	Added the division symbol to the parser, and minimal...	blob \| commitdiff \| raw \| diff to current
2010-05-19	Tim King	Significant revision to theory/arith. The new draft...	blob \| commitdiff \| raw \| diff to current
2010-04-14	Dejan Jovanović	Marging from types 404:415, changes: Massive	blob \| commitdiff \| raw \| diff to current
2010-04-13	Christopher L. Conway	Doxygen fixes	blob \| commitdiff \| raw \| diff to current
2010-04-01	Morgan Deters	reran update-copyright.pl to get new contributors and...	blob \| commitdiff \| raw \| diff to current
2010-04-01	Morgan Deters	PARSER STUFF:	blob \| commitdiff \| raw \| diff to current
2010-03-30	Morgan Deters	Highlights of this commit are:	blob \| commitdiff \| raw \| diff to current
2010-03-15	Morgan Deters	This checkin resolves bug #57.	blob \| commitdiff \| raw \| diff to current
2010-03-12	Dejan Jovanović	Fixing unnecessary construction of NOT nodes when...	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 Deters	naive 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-03-08	Dejan Jovanović	some more sat stuff for tim: assertions now go to theory_uf	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-25	Morgan Deters	* src/expr/node.h: add a copy constructor. Apparently...	blob \| commitdiff \| raw \| diff to current
2010-02-04	Morgan Deters	minor interface changes to TheoryEngine/Theory after...	blob \| commitdiff \| raw \| diff to current
2010-02-04	Morgan Deters	remove -- c++ -- emacs tag from source files (it...	blob \| commitdiff \| raw \| diff to current
2010-02-04	Morgan Deters	Added theory output channel interfaces and "Interrupted...	blob \| commitdiff \| raw \| diff to current
2009-12-17	Morgan Deters	update-copyright.pl now retrieves and incorporates...	blob \| commitdiff \| raw \| diff to current
2009-12-08	Morgan Deters	work on propositional layer, expression builder support...	blob \| commitdiff \| raw \| diff to current
2009-11-19	Morgan Deters	testing framework, configure fixes, incorporations...	blob \| commitdiff \| raw \| diff to current
2009-11-17	Morgan Deters	from meeting	blob \| commitdiff \| raw \| diff to current

RSS Atom