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

Age	Commit message (Collapse)	Author
2009-12-17	fix typos in Makefile.am for unit testing	Morgan Deters

2009-12-17	addressed some concerns raised by Clark in bug #6 (code review of driver code)	Morgan Deters

2009-12-17	making config/mkbuilddir executable	Morgan Deters

2009-12-17	Minor changes from code review	Clark Barrett

2009-12-17	build system cleanup; test system separation into white-box, black-box, and ↵	Morgan Deters
	public tests
2009-12-17	testing infrastructure fixes	Morgan Deters

2009-12-17	support nonstandard, unconfigured builds (e.g., "./configure debug" followed ↵	Morgan Deters
	by "make production ASSERTIONS=1")
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	Small refactoring changes for the expr package.	Tim King

2009-12-16	Spelling correction in comments	Christopher L. Conway

2009-12-16	Standardizing configure arguments for ANTLR/CxxTest	Christopher L. Conway

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-15	Minor changes to parser files from code review.	Christopher L. Conway

2009-12-15	Added context_mm (haven't tested compilation yet...)	Clark Barrett

2009-12-15	minor: fixing typos	Morgan Deters

2009-12-11	Extracted the public Expr and ExprManager interface to encapsulate the ↵	Dejan Jovanović
	optimized expressions and the internal expression manager.
2009-12-11	build fixes, configuration simplifications	Morgan Deters

2009-12-10	killing expr into node...	Dejan Jovanović

2009-12-10	cleanups, assert work, add a stubbed uf theory, fix driver	Morgan Deters

2009-12-09	some fixes and organizational adjustments to assert code, parsers/lexers, ↵	Morgan Deters
	and build process
2009-12-09	A mess of changes in the expression manager, simple example still failing ↵	Dejan Jovanović
	due to some problems in the prop_engine * default null expr and expr value and reorganisation/rewrite of some methods * fixed some bugs * expressions should always be passed as const Expr& to methods, otherwise copy constructors are called Problematic code: * Expr class has a bunch of methods that return Exprs, such as a.andExpr(b). None of these know what is their expression manager. We should (a) Not allow this, all expression construction should go through the ExprBuilder or directly thorugh the expression manager (b) Allow this, as it is now, but the have the default expression manager be setup in every entry into the smt solver + these construction methods shouldn't be available to the user (oterwise a mess ensues) * We have to decide how to construct ExprBuilders: (a) constructing ExprBuilders with em = ExprBuilder(e).andExpr(b) is problematic as at construction we can't know the expression manager, and the kind of em will be UNDEFINED, so when adding b we can't assume its not UNDEFINED (b) constructing it with ExprBuilder(em) << AND << a << b or ExprBuilder(em, AND) << a << b seems like a nicer approach I am still confused about these expression builders so we should talk about this.
2009-12-08	final (?) fixes to parser/generated build directory modifications	Morgan Deters

2009-12-08	parser build fixes	Morgan Deters

2009-12-08	check in automake/libtool/autoconf-generated files; add better file not ↵	Morgan Deters
	found handling
2009-12-08	broken formula	Morgan Deters

2009-12-08	work on propositional layer, expression builder support for large ↵	Morgan Deters
	expressions, output classes, and minisat
2009-12-07	fixing a few broken build-related items, adding test cases	Morgan Deters

2009-12-07	big check-in of various fixes and adjustments	Morgan Deters

2009-12-07	antlr parser for the cvc4 language (boolean only)	Dejan Jovanović
	yet to be finalized, it should work as expected
2009-12-06	Big chunk of changes:	Dejan Jovanović
	* Fixed bugs in option parsing * Simplified the main.cpp significantly (more c++ like) * Added the null kind, expr value, and expression, with the default constructor public * Simplified commands, we need to discuss this in the meeting (what to do with command results?) * Removed all the lex/yacc files * Symbol table is now a templated class, as we will have tables for variables, predicates and functions * The ANTLR parsing infrastructure/makefiles is all in. SMT lib Boolean benchmarks should parse + giving nice error such as Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test4.smt:3:16: Undeclared variable p Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test2.smt:2:11: unexpected token: sa Didn't add any unit tests as the unit testing doesn't work with the updated build system -- it doesn't know how to create directories in the corresponding build directory. TODO: * add the PL grammar and unit test when the testing becomes available * with this build setup my eclipse debugger doesn't work. Might have something to do with the visibility of symbols? * i'm getting g++ depracated warnings regarding the hash_map from the symbol table, need to figure out how to use it in a standard manner. the new <unordered_map> header is for C++0x, and the <ext/hash_map> is getting deprecation warningns... weird.
2009-12-05	more build system work	Morgan Deters

2009-12-04	more build system work	Morgan Deters

2009-12-04	More changes to configure.ac to include the smt grammar directory. The ↵	Dejan Jovanović
	parser refuses to be built in the new separate directory structure though.
2009-12-04	Forgot to commit changes to configure.ac	Dejan Jovanović

2009-12-04	Adding support for ANTLR checking in autogen.sh (config/antlr.m4). Commiting ↵	Dejan Jovanović
	antlr SMT grammar that should compile, but is not yet integrated. Tests of compilation and antlr crashes appreciated.
2009-12-03	Eclipse CVC4 settings (with code style)	Dejan Jovanović

2009-12-03	additional build system fixes	Morgan Deters

2009-12-03	first attempt at new build system	Morgan Deters

2009-12-03	parsing/expr/command/result/various other fixes	Morgan Deters

2009-12-01	svignore for parser and util	Dejan Jovanović

2009-11-28	Added an EmptyCommand and a CommandSequence commands and changed the parser ↵	Dejan Jovanović
	a bit.
2009-11-26	Commands and the eclipse C++ project settings.	Dejan Jovanović

2009-11-26	Enough parsing for tonight. Added:	Dejan Jovanović
	* Everything goes through the ParserState instead of coding in lex/yacc files * Bare Boolean SMT lexer/parser * Basic commands To be completed: ParserState method implementations, parser.h/parser.cpp, make it compile and run...
2009-11-25	additional work on parser hookup, configuration + build	Morgan Deters

2009-11-24	Missed file: symbol_table.h	Christopher L. Conway

2009-11-24	Parser should be complete for Booleans	Christopher L. Conway

2009-11-24	oops, missed a file	Morgan Deters

2009-11-24	various fixes and updates to use and support parser	Morgan Deters

2009-11-24	Stubbing commands	Christopher L. Conway

2009-11-24	Stubbing commandsmake	Christopher L. Conway