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

Age	Commit message (Collapse)	Author
2010-03-30	Merging from branches/antlr3 (r246:354)	Christopher L. Conway

2010-03-16	* test/unit/Makefile.am, test/unit/expr/attribute_white.h,	Morgan Deters
	test/unit/expr/node_white.h: add whitebox attribute test (pulled out attribute stuff from node_white) * test/unit/parser/parser_black.h: fix memory leaks uncovered by valgrind * src/theory/interrupted.h: actually make this "lightweight" (not derived from CVC4::Exception), as promised in my last commit * src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match the new-style cleanup function definition * src/expr/attribute.cpp, src/expr/attribute.h: support for attribute deletion, custom cleanup functions, clearer cleanup function definition. * src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool", and enable freeing of NodeValues * src/expr/type.h, src/expr/type.cpp: reference-counting for types, customized cleanup function for types, also code cleanup * (various): changed "const Type" to "Type" (to enable reference-counting etc. Types are still immutable.) * src/util/output.h: add ::isOn()-- which queries whether a Debug/Trace flag is currently on or not. * src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp, src/expr/type.cpp, src/expr/expr_manager.cpp, various others: minor code cleanup
2010-03-10	Adding preliminary let/flet support to SMT parser (Bug #51)	Christopher L. Conway

2010-02-06	Preliminary support for types in parser	Christopher L. Conway

2010-02-04	remove -- c++ -- emacs tag from source files (it overrides ↵	Morgan Deters
	cvc4-c++-editing-mode from contrib/editing-with-emacs
2010-02-04	minor fix for update-copyright.pl; ran update-copyright.pl on all sources; ↵	Morgan Deters
	regenerated configure script
2010-02-03	Adding functions/predicates to SMT grammar	Christopher L. Conway

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-02-02	Minor changes to parser	Christopher L. Conway

2010-02-02	Adding support for escapes in string literals (strings like "\n\t\"")	Dejan Jovanović

2009-12-17	Adding more parser tests	Christopher L. Conway

2009-12-15	Minor changes to parser files from code review.	Christopher L. Conway

2009-12-09	some fixes and organizational adjustments to assert code, parsers/lexers, ↵	Morgan Deters
	and build process