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

Age	Commit message (Collapse)	Author
2010-02-02	for tim	Dejan Jovanović

2010-02-02	Switched cnf conversion to go through CnfStream.	Tim King

2010-01-30	cnf conversion (variable-introducing), cleanups, fixes to minisat calling ↵	Morgan Deters
	for multiple-query cases
2010-01-29	Adding Makefile.in to svn:ignore	Christopher L. Conway

2010-01-29	fixed CNF conversion, and more modular; CNF conversion command line option; ↵	Morgan Deters
	various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)
2010-01-28	Removing Makefile.in's	Christopher L. Conway

2010-01-26	cnf conversion	Morgan Deters

2010-01-26	fixes to build structure, util classes, lots of fixes to Node and ↵	Morgan Deters
	NodeBuilder. outstanding SEGVs fixed
2009-12-17	update-copyright.pl now retrieves and incorporates author information from ↵	Morgan Deters
	repository history; re-ran update-copyright.pl; cleaned up some things with make
2009-12-17	coding standard fix on SmtEngine; fix recursive make	Morgan Deters

2009-12-17	+ test infrastructure fixes	Morgan Deters
	+ regenerate configure script + add CVC4::Message output class + add some IllegalArgument() assertion things + rename NodeManager::mkExpr() to mkNode()
2009-12-17	build system cleanup; test system separation into white-box, black-box, and ↵	Morgan Deters
	public tests
2009-12-17	support nonstandard, unconfigured builds (e.g., "./configure debug" followed ↵	Morgan Deters
	by "make production ASSERTIONS=1")
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	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	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	check in automake/libtool/autoconf-generated files; add better file not ↵	Morgan Deters
	found handling
2009-12-08	work on propositional layer, expression builder support for large ↵	Morgan Deters
	expressions, output classes, and minisat
2009-12-07	big check-in of various fixes and adjustments	Morgan Deters

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

2009-11-25	additional work on parser hookup, configuration + build	Morgan Deters

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	configure option adjustments as per 11/24 meeting; various fixes and ↵	Morgan Deters
	improvements
2009-11-23	fixups, file comments	Morgan Deters

2009-11-20	fixes to build/test system	Morgan Deters

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

2009-11-17	ignored items	Morgan Deters

2009-11-17	from meeting	Morgan Deters