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

Age	Commit message (Collapse)	Author
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

2011-05-01	minor fixes, plus experimental readline support in InteractiveShell	Morgan Deters

2011-04-10	merge from replay branch	Morgan Deters

2011-04-10	Add -lprofiler when --with-google-perftools is offered; also fix some ↵	Morgan Deters
	newswire-raised documentation issues.
2011-04-02	with --with-google-perftools, don't just take it on blind faith, require a ↵	Morgan Deters
	successful link at configure time
2011-03-25	This is a merge from the "theoryfixes+cdattrhash" branch. The changes	Morgan Deters
	are somewhat disparate but belonged on the same branch because they were held back from trunk all for the same reason (to keep the trunk stable for furious bitvector development). Dejan has now given me the go-ahead for a merge. ========================================= THIS COMMIT CHANGES THE THEORY INTERFACE! ========================================= Theory constructors are expected to take an additional "Valuation" parameter that each Theory should send along to the base class constructor. The base class Theory keeps the Valuation in a d_valuation field for use by it and by its derived classes. Theory::getValue() no longer takes a Valuation* (it is expected to use d_valuation instead). This allows other theory functions to take advantage of getValue() for debugging or heuristic purposes. TODO BEFORE MERGE TO TRUNK: ***implement BitIterator find() in CDAttrHash<bool>. Specifically: Added QF_BV support for SMT-LIB v2. * Two adjustments to the theory interface as requested by Tim King: 1. As described above. 2. Theories now have const access to the fact queue through base class functions facts_begin() and facts_end(); useful for debugging. * Added an "Asserted" attribute so that theories can check if something has been asserted or not (and therefore not propagate it). However, this has been disabled for now, pending more data on the overhead of it, and pending discussion at the 3/25/2011 meeting. * Do not define NDEBUG in MiniSat in assertion-enabled builds (so that MiniSat asserts are evaluated). * As a result of the new MiniSat assertions, some --incremental regressions had to be disabled; also, some bitvectors ?!! * Bug 71 is resolved by adding a specialization for CDAttrHash<> in the attribute package. * Fixes for some warnings flagged by clang. * System tests have arrived! So far mainly infrastructure for having system tests, but there is a system test aimed at improving code coverage of the printer package. * Minor other adjustments to documentation and coding to be more conformant to CVC4 policy. Tests have been performed to demonstrate that these changes have no or negligible effect on performance. In particular, changing the CDAttrHash<> doesn't have any real effect on performance or memory right now, since there is only one context-dependent boolean flag (as soon as another is added, the effect is noticeable but probably still slight).
2011-03-15	Merge from cudd branch. This mostly just adds support for linking	Morgan Deters
	against cudd libraries, the propositional_query class (in util/), which uses cudd if it's available (and otherwise answers UNKNOWN for all queries), and the arith theory support for it (currently disabled per Tim's request, so he can clean it up). Other changes include: * contrib/debug-keys - script to print all used keys under Debug(), Trace() * test/regress/run_regression - minor fix (don't export a variable) * configure.ac - replace a comment removed by dejan's google perf commit * some minor copyright/documentation updates, and minor changes to source text to make 'clang --analyze' happy.
2011-03-14	adding support for google performance tools to the build sytem, it can be ↵	Dejan Jovanović
	enabled at configure with --with-google-perftools to use it on ubuntu, you need to install packages google-perftools and libgoogle-perftools0 to run the profiling of the heap, you can run it for example with HEAPPROFILE=/tmp/profile ./builds/bin/cvc4 test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt this will create some files /tmp/profile* that you can then to get the pdf of the profile you can then run google-pprof --pdf ./builds/bin/cvc4 /tmp/profile.0001.heap > profile.pdf or for other options check http://goog-perftools.sourceforge.net/doc/
2010-12-17	tls.h, rational.h, and integer.h are only re-generated if changed. this ↵	Morgan Deters
	obviates the need for a full rebuild just because you re-./configured.
2010-11-18	small changes to documentation; also, '\''make doc'\'' doesn't build dot ↵	Morgan Deters
	graphs (but nightly build system will produce them)
2010-10-31	enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some ↵	Morgan Deters
	documentation, and make it possible to "make doc" on a clean source tree (post-configure)
2010-10-29	portability updates to build system	Morgan Deters

2010-10-28	fix confusing CXXTEST configure message, indicating success at finding ↵	Morgan Deters
	cxxtest when it wasn't found.
2010-10-12	Merge from cc-memout branch. Here are the main points	Morgan Deters
	* Add ContextMemoryAllocator<T> allocator type, conforming to STL allocator requirements. * Extend the CDList<> template to take an allocator (defaults to std::allocator<T>). * Add a specialized version of the CDList<> template (in src/context/cdlist_context_memory.h) that allocates a list in segments, in context memory. * Add "forward" headers -- cdlist_forward.h, cdmap_forward.h, and cdset_forward.h. Use these in public headers, and other places where you don't need the full header (just the forward-declaration). These types justify their own header (instead of just forward-declaring yourself), because they are complex templated types, with default template parameters, specializations, etc. * theory_engine.h no longer depends on individual theory headers. (Instead it forward-declares Theory implementations.) This is especially important now that theory .cpp files depend on TheoryEngine (to implement Theory::getValue()). Previously, any modification to any theory header file required all theories, and the engine, to be completely rebuilt. * Support memory cleanup for nontrivial CONSTANT kinds. This resolves an issue with arithmetic where memory leaked for each distinct Rational or Integer that was wrapped in a Node.
2010-10-10	additional model gen and SMT-LIBv2 compliance work: (get-assignment) now ↵	Morgan Deters
	supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
2010-10-07	type checking for define-fun in production builds; related to (and might ↵	Morgan Deters
	resolve) bug 212
2010-10-01	re-add no-deprecated to C sources; update some file-level documentation; ↵	Morgan Deters
	first look at cdvector for code review
2010-10-01	replacement implementation for clock_gettime() on mac os x, build ↵	Morgan Deters
	portability (resolving mac os x issues), code cleanup, fix compiler warnings
2010-09-30	fixed a number of problems with mac os x builds. build now works on mac os ↵	Morgan Deters
	x if you disable the clock_gettime check in configure.ac (resolves bug #202), but the parser is broken (new bug #208)
2010-09-27	add workaround for systems (i.e., Mac OS X) that don't support __thread; ↵	ACSYS
	also configure script auto-detection of __thread support and syntax
2010-09-24	roll back an unintended change with r900	Morgan Deters

2010-09-24	Fix build system for Mac OS X builds (resolves bug #203)	Morgan Deters

2010-09-02	* add TimerStat statistic type	Morgan Deters
	* add Stats black-box unit test * new make target: "make units" now runs unit tests only * revised make target: "make regress" now runs regressions only * configure.ac: pull in librt for clock_gettime()
2010-08-24	Making GMP default, CLN opt-in with --with-cln	Christopher L. Conway