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

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

2021-02-01	Andrew Reynolds	Eliminate PREPROCESS lemma property (#5827)	blob \| commitdiff \| raw
2021-01-28	Andrew Reynolds	Simplify lemma interface (#5819)	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-01	Haniel Barbosa	Removes old proof code (#4964)	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Connect the relevance manager to TheoryEngine and use...	blob \| commitdiff \| raw \| diff to current
2020-07-28	Andrew Reynolds	Use lemma property enum for OutputChannel::lemma (...	blob \| commitdiff \| raw \| diff to current
2020-06-25	Andrew Reynolds	(proof-new) Add TrustNode interfaces to OutputChannel...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-02-20	Mathias Preiner	resource manager: Add statistic for every resource...	blob \| commitdiff \| raw \| diff to current
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-04-24	Mathias Preiner	Do not use __ prefix for header guards. (#2974)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-08-17	Andrew Reynolds	Remove support for flipDecision (#2319)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-01-09	Tim King	Removing more miscellaneous throw specifiers. (#1488)	blob \| commitdiff \| raw \| diff to current
2017-11-15	Tim King	Adding garbage collection for Proof objects. (#1294)	blob \| commitdiff \| raw \| diff to current
2017-10-26	Tim King	Removing throw specifiers from OutputChannel and subcla...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2016-11-18	Tim King	Removing some throw specifiers from OutputChannel....	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-09	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-04-09	Kshitij Bansal	cardinality operation for finite sets (based on my...	blob \| commitdiff \| raw \| diff to current
2016-04-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2016-01-27	Liana Hadarean	Merged bit-vector and uf proof branch.	blob \| commitdiff \| raw \| diff to current
2016-01-09	Tim King	Adding a new Listener utility class. Changing the Resou...	blob \| commitdiff \| raw \| diff to current
2016-01-06	Tim King	Add SmtGlobals Class	blob \| commitdiff \| raw \| diff to current
2015-12-27	Clark Barrett	Merged my changes from experimental branch (new array...	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2015-05-29	lianah	changed resource step options to unsigned	blob \| commitdiff \| raw \| diff to current
2015-05-28	Liana Hadarean	added options for controlling resource step-count for...	blob \| commitdiff \| raw \| diff to current
2015-05-27	lianah	Merge pull request #75 from Dunedune/master	blob \| commitdiff \| raw \| diff to current
2015-05-22	Jordy Ruiz	Added throw LogicException to method lemma.	blob \| commitdiff \| raw \| diff to current
2014-11-27	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-11-17	Liana Hadarean	Resource-limiting work.	blob \| commitdiff \| raw \| diff to current
2014-07-10	Kshitij Bansal	Merge remote-tracking branch 'origin/master' into segfa...	blob \| commitdiff \| raw \| diff to current
2014-07-01	Morgan Deters	Update copyrights.	blob \| commitdiff \| raw \| diff to current
2014-04-01	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-26	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-07	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-03-04	Morgan Deters	Don't theory-preprocess under quantifiers; but DO theor...	blob \| commitdiff \| raw \| diff to current
2013-09-30	Liana Hadarean	merged golden	blob \| commitdiff \| raw \| diff to current
2013-09-13	Morgan Deters	Documentation fixes, some code typo fixes, file perms...	blob \| commitdiff \| raw \| diff to current
2013-05-03	Tim King	Merging branch 'soiquickexplain'.	blob \| commitdiff \| raw \| diff to current
2013-05-03	Tim King	Merge branch 'fcexplanations'	blob \| commitdiff \| raw \| diff to current
2013-05-02	Dejan Jovanović	* splitLemma to request atoms	blob \| commitdiff \| raw \| diff to current
2013-04-02	Morgan Deters	Regenerated copyrights: canonicalized names, no emails	blob \| commitdiff \| raw \| diff to current
2013-04-02	Morgan Deters	update copyrights	blob \| commitdiff \| raw \| diff to current
2013-04-01	Tim King	Adding demand restart.	blob \| commitdiff \| raw \| diff to current
2013-04-01	Morgan Deters	Merging some cleanup work:	blob \| commitdiff \| raw \| diff to current
2012-10-11	Morgan Deters	Standardizing copyright notice. Touches ALL source...	blob \| commitdiff \| raw \| diff to current
2012-09-28	Morgan Deters	rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert...	blob \| commitdiff \| raw \| diff to current
2012-08-31	Andrew Reynolds	merge from fmf-devel branch. more updates to models...	blob \| commitdiff \| raw \| diff to current
2012-08-16	Morgan Deters	Replace propagateAsDecision() with Theory::getNextDecis...	blob \| commitdiff \| raw \| diff to current
2012-06-11	Morgan Deters	Merge from quantifiers2-trunkmerge branch.	blob \| commitdiff \| raw \| diff to current
2012-06-06	Dejan Jovanović	Changes to the combination mechanism, lots of details...	blob \| commitdiff \| raw \| diff to current
2012-02-22	Morgan Deters	Added OutputChannel::propagateAsDecision() functionalit...	blob \| commitdiff \| raw \| diff to current
2011-12-06	Morgan Deters	LemmaStatus changes, as agreed to during 12/2 meeting.	blob \| commitdiff \| raw \| diff to current
2011-10-23	Morgan Deters	Implement changes from yesterday morning's meeting...	blob \| commitdiff \| raw \| diff to current
2011-10-13	Morgan Deters	Interruption, time-out, and deterministic time-out...	blob \| commitdiff \| raw \| diff to current
2011-09-15	Dejan Jovanović	additional stuff for sharing,	blob \| commitdiff \| raw \| diff to current
2011-09-02	Morgan Deters	Merge from my post-smtcomp branch. Includes:	blob \| commitdiff \| raw \| diff to current
2011-09-02	Morgan Deters	Partial merge of integers work; this is simple B&B...	blob \| commitdiff \| raw \| diff to current
2011-08-27	Dejan Jovanović	Removing Theory::registerTerm() as discussed in the...	blob \| commitdiff \| raw \| diff to current
2011-04-14	Morgan Deters	Three things:	blob \| commitdiff \| raw \| diff to current
2011-04-04	Morgan Deters	Add documentation to Node and TNode (closes bug #201).	blob \| commitdiff \| raw \| diff to current
2010-11-19	Morgan Deters	Merge from ufprop branch, including:	blob \| commitdiff \| raw \| diff to current
2010-11-09	Dejan Jovanović	Lemmas on demand work, push-pop, some cleanup.	blob \| commitdiff \| raw \| diff to current
2010-10-24	Morgan Deters	add a CVC4_UNDEFINED keyword, for intentionally undefin...	blob \| commitdiff \| raw \| diff to current
2010-10-12	Morgan Deters	hooked up "we are incomplete" flag after conversation...	blob \| commitdiff \| raw \| diff to current
2010-10-05	Morgan Deters	parser and core support for SMT-LIBv2 commands get...	blob \| commitdiff \| raw \| diff to current
2010-10-03	Morgan Deters	file header documentation regenerated with contributors...	blob \| commitdiff \| raw \| diff to current
2010-07-06	Clark Barrett	Moved registration to theory engine	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-27	Tim King	Preregistration has been turned on. Highly experimental...	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_builder.h: fixed some overly-aggressive...	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-22	Morgan Deters	Re-committing revision 232 properly:	blob \| commitdiff \| raw \| diff to current
2010-02-22	Morgan Deters	undoing 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-04	Morgan Deters	remove -- c++ -- emacs tag from source files (it...	blob \| commitdiff \| raw \| diff to current
2010-02-04	Morgan Deters	minor fix for update-copyright.pl; ran update-copyright...	blob \| commitdiff \| raw \| diff to current
2010-02-04	Morgan Deters	Added theory output channel interfaces and "Interrupted...	blob \| commitdiff \| raw \| diff to current

RSS Atom