cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2010-09-02	* add TimerStat statistic type	Morgan Deters
	* add Stats black-box unit test * new make target: "make units" now runs unit tests only * revised make target: "make regress" now runs regressions only * configure.ac: pull in librt for clock_gettime()
2010-07-04	make dist && make distcheck functional, other fixes	Morgan Deters

2010-06-15	fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)	Morgan Deters

2010-06-15	remove warnings about unknown #pragma GCC diagnostic on older compilers	Morgan Deters

2010-04-14	* Better dependency tracking for unit test building and linking, and	Morgan Deters
	auto-generated headers (metakind.h etc.), so they don't have to be recompiled every time. This drastically improves build time when only small updates are made. * Added "memory.h" unit test header for checking out-of-memory conditions. cdlist_black uses it. * Added helpful output when you "make lcov" in a non-coverage-enabled build. * Removed strict aliasing warning when compiling metakind.h header with optimization on. * Removed const version of NodeBuilder::operator Node()---it was poorly performing, better to not permit it---and fixed the convenience builders to use the non-const version (re: code review #63) * Color-coded test output on capable terminals. * Fixed some warnings in unit tests.
2010-04-09	minor fixes to lcov build target, better contextobj testing	Morgan Deters

2010-04-09	added experimental "make lcov" target (it runs only unit tests); better ↵	Morgan Deters
	coverage for util and context classes; implemented some output functionality that was missing; reclassified some tests white -> black or black -> public; other minor fixes
2010-03-08	This fixes regressions at levels >= 1 which were failing	Morgan Deters
	* implement zombification and garbage collection of NodeValues (but GC not turned on yet) * implement removal of key nodes from all attribute tables * audit NodeBuilder and fix memory leaks and improper reference-count management. This is in many places a re-write. Clearly documented invariants on NodeBuilder state. (Closes Bug 38) * created a "BackedNodeBuilder" that can be used to construct NodeBuilders with a stack-based backing store for a size that's not a compile-time constant. * NodeValues no longer depend on Node for toStream()'ing * make unit test-building "silent" with --enable-silent-rules * (Makefile.am, Makefile.builds.in) fix top-level build system so that "make regressN" works with unbuilt/out-of-date source trees in the expected way. * (various) code cleanup, documentation, formatting
2010-02-18	Rm'ing doc from SUBDIRS	Christopher L. Conway

2010-02-18	Adding doxygen configuration parameters and doxygen-doc Makefile target	Christopher L. Conway

2010-02-05	remove the last vestiges of support for "make build-profile" without first ↵	Morgan Deters
	configuring the build-profile, simplifying the build process and closing bug 21
2010-02-04	build system for multi-level regressions	Morgan Deters

2009-12-17	coding standard fix on SmtEngine; fix recursive make	Morgan Deters

2009-12-17	support nonstandard, unconfigured builds (e.g., "./configure debug" followed ↵	Morgan Deters
	by "make production ASSERTIONS=1")
2009-12-05	more build system work	Morgan Deters

2009-11-25	additional work on parser hookup, configuration + build	Morgan Deters

2009-11-20	fixes to build/test system	Morgan Deters

2009-11-19	testing framework, configure fixes, incorporations from meeting, continued work	Morgan Deters

2009-11-17	fixes/redesign of source layout from meeting	Morgan Deters

2009-11-12	parser, minisat, other things..	Morgan Deters

2009-11-09	minor fixes, added contrib directory	Morgan Deters

2009-11-03	commit of project structure including autotools support	Morgan Deters