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

Age	Commit message (Collapse)	Author
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-22	fix bug 33 (statically link the "cvc4" binary); also main driver cleanup	Morgan Deters

2010-02-03	Addressed many of the concerns of bug 10 (build system code review).	Morgan Deters
	Some parts split into other bugs: 19, 20, 21. Addressed concerns of bug 11 (util package code review). Slight parser source file modifications: file comments, #included headers in generated parsers/lexers Added CVC4::Result propagation back through MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when verbosity is not requested.
2010-01-26	fixes to build structure, util classes, lots of fixes to Node and ↵	Morgan Deters
	NodeBuilder. outstanding SEGVs fixed
2009-12-17	coding standard fix on SmtEngine; fix recursive make	Morgan Deters

2009-12-08	work on propositional layer, expression builder support for large ↵	Morgan Deters
	expressions, output classes, and minisat
2009-12-05	more build system work	Morgan Deters