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

[cvc5.git] / src / expr / node_manager.h

2013-09-09	Morgan Deters	Support empty (and 1-ary) tuples and records.	blob \| commitdiff \| raw
2013-09-05	Morgan Deters	Fix declare-fun/define-fun in dumps; resolves bugs...	blob \| commitdiff \| raw \| diff to current
2013-08-26	Kshitij Bansal	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-07-11	Morgan Deters	Support for TPTP's TFF0 (with arithmetic)	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
2012-12-01	Morgan Deters	Fix the way abstract values are typed; fixes some compl...	blob \| commitdiff \| raw \| diff to current
2012-11-29	Kshitij Bansal	Hack to support global variables for CVC language exten...	blob \| commitdiff \| raw \| diff to current
2012-11-27	Morgan Deters	First chunk of boolean-terms support.	blob \| commitdiff \| raw \| diff to current
2012-11-27	Morgan Deters	Tuples and records merge. Resolves bug 270.	blob \| commitdiff \| raw \| diff to current
2012-10-11	Morgan Deters	Standardizing copyright notice. Touches ALL source...	blob \| commitdiff \| raw \| diff to current
2012-10-11	Morgan Deters	Fix wording on GPL in legal notices; also remove an...	blob \| commitdiff \| raw \| diff to current
2012-09-26	Morgan Deters	The Tuesday Afternoon Catch-All Commit (TACAC):	blob \| commitdiff \| raw \| diff to current
2012-09-24	Dejan Jovanović	some api changes	blob \| commitdiff \| raw \| diff to current
2012-09-19	Morgan Deters	General subscriber infrastructure for NodeManager,...	blob \| commitdiff \| raw \| diff to current
2012-08-24	Morgan Deters	* disallow internal uses of mkVar() (you have to mkSkol...	blob \| commitdiff \| raw \| diff to current
2012-08-24	Morgan Deters	fix get-value output in a couple ways; this fixes bug...	blob \| commitdiff \| raw \| diff to current
2012-08-13	Morgan Deters	Minor cleanup. No performance difference expected.	blob \| commitdiff \| raw \| diff to current
2012-08-07	Morgan Deters	Some items from the CVC4 public interface review:	blob \| commitdiff \| raw \| diff to current
2012-08-03	Morgan Deters	fix uses of getMetaKind() from outside the expr package...	blob \| commitdiff \| raw \| diff to current
2012-07-31	Morgan Deters	Options merge. This commit:	blob \| commitdiff \| raw \| diff to current
2012-07-16	Morgan Deters	Support for having two SmtEngines with the same ExprMan...	blob \| commitdiff \| raw \| diff to current
2012-07-07	Morgan Deters	Various fixes to documentation---typos, some incomplete...	blob \| commitdiff \| raw \| diff to current
2012-06-12	Morgan Deters	minor cleanup, and replace a "private:" in equality...	blob \| commitdiff \| raw \| diff to current
2012-06-11	Morgan Deters	Merge from quantifiers2-trunkmerge branch.	blob \| commitdiff \| raw \| diff to current
2012-05-18	Tim King	This commit adds TypeNode::leastCommonTypeNode(). ...	blob \| commitdiff \| raw \| diff to current
2012-05-18	Tim King	This commit removes the dead psuedoboolean code.	blob \| commitdiff \| raw \| diff to current
2012-05-11	Morgan Deters	output a warning message when a function type (or datat...	blob \| commitdiff \| raw \| diff to current
2012-04-18	Dejan Jovanović	disabling the problematic pragma in node_manager.h...	blob \| commitdiff \| raw \| diff to current
2012-04-17	Dejan Jovanović	Fix for thos annoying "array index" warnings in product...	blob \| commitdiff \| raw \| diff to current
2012-03-01	Morgan Deters	Partial merge from kind-backend branch, including Minis...	blob \| commitdiff \| raw \| diff to current
2012-02-23	Morgan Deters	Added ability to set a "cvc4-specific logic" in standar...	blob \| commitdiff \| raw \| diff to current
2012-02-20	Morgan Deters	portfolio merge	blob \| commitdiff \| raw \| diff to current
2011-11-16	Morgan Deters	Addressed many of the concerns raised in the public...	blob \| commitdiff \| raw \| diff to current
2011-11-04	Morgan Deters	STRING_TYPE and CONST_STRING and associate type infrast...	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-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-06-30	Morgan Deters	only use theory registration if (1) a theory requests...	blob \| commitdiff \| raw \| diff to current
2011-06-06	Morgan Deters	Fix for Mac OS breakage (x86 didn't crash, but probably...	blob \| commitdiff \| raw \| diff to current
2011-05-14	Morgan Deters	reverting node manager change from 1881; also part...	blob \| commitdiff \| raw \| diff to current
2011-05-13	Andrew Reynolds	added support for parametric datatypes, updated cvc...	blob \| commitdiff \| raw \| diff to current
2011-04-20	Morgan Deters	Tuesday end-of-day commit.	blob \| commitdiff \| raw \| diff to current
2011-04-18	Morgan Deters	mostly CVC presentation language parsing and printing	blob \| commitdiff \| raw \| diff to current
2011-04-18	Morgan Deters	Partial merge from datatypes-merge branch:	blob \| commitdiff \| raw \| diff to current
2011-04-15	Morgan Deters	partial merge from portfolio branch, adding conversions...	blob \| commitdiff \| raw \| diff to current
2011-04-01	Morgan Deters	This commit is a merge from the "betterstats" branch...	blob \| commitdiff \| raw \| diff to current
2011-03-25	Morgan Deters	This is a merge from the "theoryfixes+cdattrhash" branc...	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-12-14	Morgan Deters	congruence closure module now supports things other...	blob \| commitdiff \| raw \| diff to current
2010-10-28	Christopher L. Conway	Changing NodeBuilder::debugCheckType() to maybeCheckType()	blob \| commitdiff \| raw \| diff to current
2010-10-27	Christopher L. Conway	Modifying getType to use a non-recursive algorithm...	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-22	Morgan Deters	comment out the "interactive" check in SmtEngine::getVa...	blob \| commitdiff \| raw \| diff to current
2010-10-08	Morgan Deters	* (define-fun...) now has proper type checking in non...	blob \| commitdiff \| raw \| diff to current
2010-10-07	Morgan Deters	type checking for define-fun in production builds;...	blob \| commitdiff \| raw \| diff to current
2010-10-06	Morgan Deters	declare-sort, define-sort working but not thoroughly...	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-09-28	Morgan Deters	fix TLS support for platforms (e.g. Mac OS X) where...	blob \| commitdiff \| raw \| diff to current
2010-09-27	ACSYS	add workaround for systems (i.e., Mac OS X) that don...	blob \| commitdiff \| raw \| diff to current
2010-09-21	Morgan Deters	remove assertion in TNode destructor and ensure all...	blob \| commitdiff \| raw \| diff to current
2010-09-21	Christopher L. Conway	Moving automatic type check to NodeBuilder (Fixes:...	blob \| commitdiff \| raw \| diff to current
2010-09-20	Dejan Jovanović	bitvector rewriting for the core theory and testcases	blob \| commitdiff \| raw \| diff to current
2010-08-17	Morgan Deters	Merge from "cc" branch:	blob \| commitdiff \| raw \| diff to current
2010-07-29	Christopher L. Conway	Adding configuration_private.h to allow inlining of...	blob \| commitdiff \| raw \| diff to current
2010-07-28	Christopher L. Conway	Forcing a type check on Node construction in debug...	blob \| commitdiff \| raw \| diff to current
2010-07-27	Christopher L. Conway	Adding optional 'check' parameter to getType() methods	blob \| commitdiff \| raw \| diff to current
2010-07-06	Morgan Deters	Don't eagerly collect zombies. This should speed up...	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-16	Tim King	This commit just contains miscellaneous arithmetic...	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-31	Christopher L. Conway	First draft implementation of mkAssociative	blob \| commitdiff \| raw \| diff to current
2010-05-27	Morgan Deters	fix bug #134: infinite deallocation loop	blob \| commitdiff \| raw \| diff to current
2010-05-27	Morgan Deters	Remove isAtomic() as per 4/27/2010 meeting. Add commen...	blob \| commitdiff \| raw \| diff to current
2010-05-27	Christopher L. Conway	Adding NodeManager::prepareToBeDestroyed() (Fixes:...	blob \| commitdiff \| raw \| diff to current
2010-05-13	Christopher L. Conway	Minor refactorings and corrections to comments	blob \| commitdiff \| raw \| diff to current
2010-05-04	Dejan Jovanović	Type-checking classes and hooks (not tested yet).	blob \| commitdiff \| raw \| diff to current
2010-05-02	Dejan Jovanović	smt parser for bit-vectors	blob \| commitdiff \| raw \| diff to current
2010-05-01	Dejan Jovanović	Fix for the last night's build errors (type that broke...	blob \| commitdiff \| raw \| diff to current
2010-04-30	Dejan Jovanović	Fix for bug 115, mapping was going in the wrong direction.	blob \| commitdiff \| raw \| diff to current
2010-04-29	Dejan Jovanović	Added the capability to construct expressions by passin...	blob \| commitdiff \| raw \| diff to current
2010-04-26	Dejan Jovanović	Some cleanup. Also added the integer and real types.	blob \| commitdiff \| raw \| diff to current
2010-04-26	Dejan Jovanović	Adding the intermediary TypeNode to represent (and...	blob \| commitdiff \| raw \| diff to current
2010-04-15	Christopher L. Conway	Enhancements to NodeManager tests, taking advantage...	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-06	Morgan Deters	* Add some protected ContextObj accessors for ContextOb...	blob \| commitdiff \| raw \| diff to current
2010-04-05	Christopher L. Conway	Adding black-box tests for NodeManager (Closes bug...	blob \| commitdiff \| raw \| diff to current
2010-04-05	Christopher L. Conway	Minor refactorings, in response to code review (Bug...	blob \| commitdiff \| raw \| diff to current
2010-04-05	Christopher L. Conway	Typos and renames for code review	blob \| commitdiff \| raw \| diff to current
2010-04-04	Morgan Deters	* Addressed issues brought up in Chris's review of...	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 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-31	Christopher L. Conway	Finishing parser cleanup. Code is now review-ready.	blob \| commitdiff \| raw \| diff to current
2010-03-30	Morgan Deters	I think this finishes off the CDMap<>/Attribute leaks	blob \| commitdiff \| raw \| diff to current
2010-03-30	Morgan Deters	Highlights of this commit are:	blob \| commitdiff \| raw \| diff to current
2010-03-25	Christopher L. Conway	Adding comments to NodeManager	blob \| commitdiff \| raw \| diff to current
next

RSS Atom