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

Age	Commit message (Collapse)	Author
2014-06-19	Fix for mac readline.	Morgan Deters

2014-06-19	Fix for pre-C++11 is_sorted().	Morgan Deters

2014-06-19	No more dependence on libstdc++ or PBDS stuff: remove build stuff that ↵	Morgan Deters
	supported it.
2014-06-19	get-glpk-cut-log script, and configure code.	Morgan Deters

2014-06-11	Some clean-up, post bv-merge.	Morgan Deters
	Add abc to build id and fix static building. Add abc to --show-config output and Configuration class API. Add ability to select abc source path. Fix arch_flags for abc.
2014-06-10	Merging CAV14 paper bit-vector work.	lianah

2014-05-30	Fix personal.mk for some make targets.	Morgan Deters

2014-01-08	Merge branch '1.3.x'	Morgan Deters
	Conflicts: COPYING NEWS config/cvc4.m4
2014-01-08	Switch license default back to BSD, and add --best and --enable-gpl options.	Morgan Deters

2013-12-23	Proof-checking code; fixups of segfaults and missing functionality in proof ↵	Morgan Deters
	generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but not --check-proofs, since LFSC code uses globals) * proofs are not yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-12-18	Merge branch '1.3.x'	Morgan Deters
	[skip ci]
2013-12-18	Fix an autoconf issue with CLN in some configurations; also clarification ↵	Morgan Deters
	re: license issues [skip ci]
2013-12-18	Merge branch '1.3.x'	Morgan Deters

2013-12-18	Fix configure handling for CLN (should fix win32 nightly builds)	Morgan Deters

2013-12-18	Reduce autoconf version for dependence (should fix 32-bit builds).	Morgan Deters

2013-12-17	Merge branch '1.3.x'	Morgan Deters

2013-12-17	configure --with-portfolio disables CLN.	Morgan Deters

2013-12-17	Merge branch '1.3.x'	Morgan Deters
	Conflicts: COPYING NEWS
2013-12-17	some config changes: new --bsd option, readline gives warning, default build ↵	Morgan Deters
	is now production.
2013-12-16	First attempt at incorporating LFSC proof checker into CVC4.	Morgan Deters

2013-12-10	GLPK build identifier, license warnings.	Morgan Deters

2013-12-09	GLPK build identifier, license warnings.	Morgan Deters

2013-12-06	Initializing master for next version.	Morgan Deters

2013-12-06	Initializing 1.3.x branch.	Morgan Deters

2013-12-06	Cutting release 1.3.1.3	Morgan Deters

2013-11-14	Minor fixes for Mac OS Mavericks	Morgan Deters

2013-11-12	Some additional explanation for a common configure error.	Morgan Deters

2013-11-10	Flatten libcvc4 build structure; remove some #include interdependences	Morgan Deters

2013-09-18	Support a personal build configuration and make rules.	Morgan Deters

2013-07-29	Fix numerous compiler warnings on various platforms	Morgan Deters

2013-07-23	fix for win32 option parsing via mingw32	Morgan Deters

2013-05-08	Prerelease versioning for master	Morgan Deters

2013-05-08	Prerelease versioning for 1.2.x	Morgan Deters

2013-05-08	Cutting release 1.2.1.2	Morgan Deters

2013-04-29	Some fixes for GCC 4.2, and for Java on Mac	Morgan Deters

2013-04-29	Fixes to FCSimplex for some versions of compilers	Morgan Deters

2013-04-26	FCSimplex branch merge	Tim King

2013-04-23	Theory "alternates" support	Morgan Deters
	* This is a feature that Dejan and I want for the upcoming tutorial. It allows rapid prototyping of new decision procedure implementations (which we may choose to demonstrate), and a new --use-theory command-line option to select from different available implementations. It has no affect on the current set of theories, as no "alternates" are defined. * Also update the new-theory script, which was broken and incomplete.
2013-04-03	Prerelease versioning for master.	Morgan Deters

2013-04-03	Pre-release versioning	Morgan Deters

2013-04-03	Cutting release 1.1.1.1	Morgan Deters

2013-04-01	Merging some cleanup work:	Morgan Deters
	* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
2013-03-26	Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac	Morgan Deters

2013-03-19	Remove PropositionalQuery class and all CUDD-related build stuff (and ↵	Morgan Deters
	references)
2013-01-28	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

2013-01-24	Add win32 support (merge from mdeters/win32, with some cleanup).	Morgan Deters

2012-12-18	Fix bug 483: readline checks must come after Boost checks in configure	Morgan Deters

2012-12-03	version numbering	Morgan Deters

2012-12-01	Cutting release 1.0.1.0	Morgan Deters

2012-11-29	Fix for hidden symbols in library on Mac. It's a strange issue to do with	Morgan Deters
	explicit template instantiation rules, -fvisibility=hidden, and the way that Apple distributes libstdc++. (this commit was certified error- and warning-free by the test-and-commit script.)