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

Age	Commit message (Collapse)	Author
2012-09-29	draft RELEASE-NOTES file, and minor release stuff	Morgan Deters

2012-09-28	Public interface review items:	Morgan Deters
	* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument() * Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only * CheckArgument() throws non-AssertionException * things outside the core library (parsers, driver) use regular C-style assert, or a public exception type. * auto-generated documentation for Smt options and internal options Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
2012-09-25	fix	Morgan Deters

2012-09-25	fix some Mac issues	Morgan Deters

2012-09-21	SMT-LIBv2 compliance updates:	Morgan Deters
	* chainability of =, <, <=, >, >= via the new CHAINABLE kind and TheoryBuiltin rewriter support (resolves bug #383) * with --smtlib2, force interactive mode off by default Also: * fix a few bugs causing crashes * better "alias" processing for options * configure-time fixes to readline detection (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-14	Fix a few minor issues in options processing, improving usability, ↵	Morgan Deters
	consistency, error-reporting, and documentation.
2012-09-04	Accepted some patches from the Multicore Programming Group at Imperial ↵	Morgan Deters
	College London (via Peter Collingbourne): cvc4-0001-Look-for-cxxtestgen-as-well-as-cxxtestgen.pl-and-cxx.patch * better checking for cxxtest cvc4-0002-Do-not-read-an-additional-command-after-failure.patch * more correct failure behavior for interactive tools cvc4-0003-Only-exit-when-encountering-a-CommandFailure.patch * don't consider "unsupported" as a failure (accepted with modifications) cvc4-0004-Produce-SMT-LIB-v2-conformant-output-for-get-info.patch * better get-info responses (accepted with modifications) These patches will help the group build Boogie support for CVC4. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-28	fix regression tests for automake 1.11 and automake 1.12---both versions ↵	Morgan Deters
	should work now
2012-08-28	fixes for Mac and automake 1.12 detection	Morgan Deters

2012-08-06	Support setting :regular-output-channel and :diagnostic-output-channel.	Morgan Deters
	Also some cleanup of option-related exceptions infrastructure.
2012-07-31	Options merge. This commit:	Morgan Deters
	1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options) 2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace. 3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..) The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options: * to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp. * to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser(). * ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options) * this point is important. If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file * Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true). Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double). For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h). Benefits of the new options system include: 1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed). 2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.) 3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc. 4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.) 5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose I've taken lots of care not to break anything. Hopefully, I've succeeded in that.
2012-07-16	reverse the order of link arguments to -lcln -lgmp, fixes linking errors for ↵	Morgan Deters
	static-binary CLN-enabled builds on greed
2012-07-08	remove a debugging line from configure script that was left in inadvertently	Morgan Deters

2012-07-01	Some changes to configure.ac:	Morgan Deters
	1. Includes BOOST_CPPFLAGS during compilation of all files, not just portfolio-relevant files. This is necessary since we now have a general dependence on Boost (not just its threading stuff). This resolves bug 357. 2. Support --disable-thread-support and --enable-thread-support, in an effort to get to the bottom of bug 361. These changes shouldn't affect performance, though #1 will build the cvc4 libs with a couple of pthread definitions that conceivably could change the behavior of #included standard headers. Let's keep an eye on tonight's regressions.
2012-06-06	Fixing numerous issues with tests and "make dist":	Morgan Deters
	* test/regress/regress0/unconstrained wasn't being distributed. This caused the debian build failure last night. (It still doesn't run on "make check", but had to be distributed properly.) * Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format. (Told automake to use a newer tar format.)
2012-04-28	require boost library (but not the threading support---that's only necessary ↵	Morgan Deters
	for portfolio)
2012-04-11	merge from arrays-clark branch	Morgan Deters

2012-04-06	fix distributed builds (and therefore the Debian nightly build) by ignoring ↵	Morgan Deters
	Makefile.am files under src/prop/cryptominisat.
2012-03-30	some more build system fixes	Dejan Jovanović

2012-03-09	Some work on the dump infrastructure to support portfolio work.	Morgan Deters
	Dump("foo") << FooCommand(...); now "dumps" the textual representation of the command (in the current output language) to a file, IF dumping is on at configure-time, AND the "muzzle" feature is off, AND the "foo" flag is turned on for the dump stream during this run. If it's a portfolio build, the above will also store the command in a CommandSequence, IF the "foo" flag is turned on for the dump stream during this run. This is done even if the muzzle is on. This commit also cleans up some code that used the dump feature (in arrays, particularly).
2012-03-03	Changing the dependency checking; GMP is required (and sometimes must be ↵	Morgan Deters
	explicitly linked in with -l) when using CLN. Fixes a bug on recent Debian that Francois reported. Hopefully this doesn't break anything..
2012-02-23	pcvc4 only built if --with-portfolio given to the configure script ↵	Morgan Deters
	(Clark-requested change)
2012-02-22	fixes to configure and boost.m4 to make certain boost installations nonfatal ↵	Morgan Deters
	errors; threading support should only be required to build pcvc4, not cvc4
2012-02-22	another static library unavailability issue	Morgan Deters

2012-02-22	Fixes to documentation / fixes for MacOS	Morgan Deters

2012-02-21	add a "--with-portfolio" configure option that makes a missing boost-thread ↵	Morgan Deters
	library an error; useful for builds requiring a "pcvc4" binary at the end
2012-02-21	fix src/util/hash.h to specialize GNU's hash template for <uint64_t> on ↵	Morgan Deters
	platforms that need it; fixes Mac builds.
2012-02-21	don't require libboost_thread (its presence is detected at configure-time), ↵	Morgan Deters
	and other build/documentation fixes from yesterday's portfolio merge; resolves bug 302
2012-02-20	zlib not required; remove configure's dependency on it	Morgan Deters

2012-02-20	portfolio merge	Morgan Deters

2012-02-12	separate new-theory components into a "theoryskel" directory so that new ↵	Morgan Deters
	files can be added to it without modifying the script.
2012-02-07	re-adding comment about available languages	Morgan Deters

2012-02-03	updating configure to use python-config for building python bindings	Dejan Jovanović

2011-10-28	proof regressions	Morgan Deters

2011-10-28	merged the proofgen3 branch into trunk:	Liana Hadarean
	- can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof.
2011-10-21	add gcc version information to Configuration, and warn when building with ↵	Morgan Deters
	v4.5.1 which has a buggy optimizer (resolves bug #266)
2011-10-19	fix configure step on Ubuntu oneiric (11.10)-- related to bug #284	Morgan Deters

2011-10-03	user push/pop support in minisat and simplification; also bindings work	Morgan Deters

2011-09-30	interfaces fixes and cleanups...and examples of each interface!	Morgan Deters

2011-09-28	better fix for #281, also fix issue with command line options not existing ↵	Morgan Deters
	on older g++en, like Apple's 4.2 on Snow Leopard.
2011-09-25	first crack at compatibility java interface (not built by default)	Morgan Deters

2011-09-21	Java binding now working. Some interface types still need some work (e.g. ↵	Morgan Deters
	iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.
2011-09-21	considerable bindings interface work, some improvements to build	Morgan Deters

2011-09-18	cleaned up the mechanism for library versioning	Morgan Deters

2011-09-16	fix debian build without breaking anything (i hope)	Morgan Deters

2011-09-03	this should fix the build; doxygen documentation now gets built in ↵	Morgan Deters
	srcdir/doc/doxygen
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.
2011-07-07	cudd-building prefs with --with-cudd / --without-cudd	Morgan Deters

2011-06-18	Some fixes inspired by Fedora 15:	Morgan Deters
	* compilation fixes for GCC 4.6.x + ptrdiff_t is now in std:: * fix some make rules that are ok in Make 3.81 but broke in Make 3.82 * look for cxxtestgen.py as well as cxxtestgen.pl, and look for cxxtest headers in /usr/include
2011-05-02	more minor fixes related to last few commits	Morgan Deters