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

Age	Commit message (Collapse)	Author
2011-09-02	Merge from my post-smtcomp branch. Includes:	Morgan Deters
	Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2010-04-01	PARSER STUFF:	Morgan Deters
	* Other minor changes to the new parser to match coding guidelines, add documentation, .... * Add CFLAGS stuff to configure.ac parser Makefile.ams. This ensures that profiling, coverage, optimization, debugging, and warning level options will apply to the new parser as well (which is in C, not C++). This fixes the deprecated warning we were seeing this evening. * Now, if you have ANTLR_HOME set in your environment, you don't need to specify --with-antlr-dir to ./configure or have libantlr3c installed in standard places. --with-antlr-dir still overrides $ANTLR_HOME, and if the installation in $ANTLR_HOME is missing or doesn't work, the standard places are still tried. * Extend "silent make" to new parser stuff. * Added src/parser/bounded_token_buffer.{h,cpp} to the list of exclusions in contrib/update-copyright.pl and mention them as excluded from CVC4 copyright in COPYING. They are antlr3-derived works, covered under a BSD license. OTHER STUFF: * expr_manager.h, expr.h, expr_manager.cpp, and expr.cpp are now auto-generated by a "mkexpr" script. This provides the correct instantiations of mkConst() for public use, e.g., by the parser. * Fix doxygen documentation in expr, expr_manager.. closes bug #35 * Node::isAtomic() implemented in a better way, based on theory kinds files. Fixes bug #40. To support this, a "nonatomic_operator" command has been added. All other "parameterized" or "operator" kinds are atomic. * Added expr_black test * Remove kind::TRUE and kind::FALSE and make a new CONST_BOOLEAN kind that takes a "bool" payload; for example, to make "true" you now do nodeManager->mkConst(true). * Make new "cvc4_public.h" and "cvc4parser_public.h" headers. Private headers should include "cvc4_private.h" (resp. "cvc4parser_private.h"), which existed previously. Public headers should include the others. No one should include the autoheader #include (which has been renamed "cvc4autoconfig.h") directly, and public CVC4 headers can't access its #defines. This is to avoid us having the same distribution problem as libantlr3c. * Preliminary fixes based on Tim's code review of attributes (bug #61). This includes splitting hairy template internals into attribute_internals.h, for which another code review ticket will be opened. Bug is still outstanding, but pending further refactoring/documentation. * Some HashFcns renamed to HashStrategy to match refactoring done elsewhere (done by Chris?) earlier this week. * Simplified creation of make rules for generated files (expr.cpp, expr.h, expr_manager.cpp, expr_manager.h, theoryof_table.h, kind.h, metakind.h). * CVC4::Configuration interface and implementation split (so private stuff doesn't leak into public headers). * Some documentation/code formatting fixes. * Add required versions of autotools to autogen.sh. * src/expr/mkmetakind: fix a nonportable thing in invocation of "expr" that was causing warnings on Red Hat. * src/context/cdmap.h: add workaround to what appears to be a g++ 4.1 parsing bug.
2010-01-28	Replacing hand-coded autogen.sh with buildconf version	Christopher L. Conway

2009-12-16	+ refactoring fixes for expr package based on code review (see bug #4)	Morgan Deters
	+ minor autogen/configure fixes for old versions of autotools
2009-12-16	Fixes to the build system:	Morgan Deters
	Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS Makefile files in src/ - support "make" under src/ (current build profile) configure.ac - updates to fix warnings config/antlr.m4 - updates to fix warnings autogen.sh - updates to generate warnings from autotools; also support Macs src/include/cvc4_config.h - guard with #ifdef total reimplementation of NodeBuilder ExprValue => NodeValue context_mm.{h,cpp} - fixed numerous compile errors
2009-12-11	build fixes, configuration simplifications	Morgan Deters

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

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

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

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