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

Age	Commit message (Collapse)	Author
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-02-19	* Attribute infrastructure -- static design. Documentation is coming.	Morgan Deters
	See test/unit/expr/node_white.h for use examples, including how to define new attribute kinds. Also: * fixes to test infrastructure * minor changes to code formatting throughout * attribute tests in test/unit/expr/node_white.h * fixes to NodeManagerScope ordering * use NodeValue::getKind() to properly deal with UNDEFINED_KIND (removing compiler warning) * ExprManager: add proper NodeManagerScope to public-facing member functions * store variable names and types in attributes * SoftNode is a placeholder, not a real implementation
2010-01-27	support "make check" in src/ subdirs for unit-testing of just that module; ↵	Morgan Deters
	also support synonyms for "make check" globally
2010-01-27	test framework fixes; bug 13 closed	Morgan Deters