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

Age	Commit message (Collapse)	Author
2014-08-25	Fix build rule.	Morgan Deters

2014-08-23	Quieter finish to build.	Morgan Deters

2014-08-09	Fix a build issue for some configurations, thanks Tianyi.	Morgan Deters

2014-08-07	Another build fix.	Morgan Deters

2014-08-07	Fix win32 build.	Morgan Deters

2014-08-06	Fix double-linking issue (I think) by simplifying builds/ structure.	Morgan Deters

2013-12-16	First attempt at incorporating LFSC proof checker into CVC4.	Morgan Deters

2013-02-15	Merge branch '1.0.x'	Morgan Deters

2013-02-15	Fix builds/ links to survive configuring twice with different prefixes	Morgan Deters

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

2012-11-26	Makefile fix for new versions of Make (thanks Clark for noticing this); see ↵	Morgan Deters
	e.g. http://osdir.com/ml/bug-make-gnu/2011-04/msg00011.html
2012-11-15	fix for "make examples"	Morgan Deters

2012-10-25	more minor fixes to build system	ACSYS

2012-10-24	Includes many fixes to build system for Solaris (thanks Tim!), and also	Morgan Deters
	just in general, and some documentation adjustments.
2012-10-03	better documentation, allow examples to be installed, etc	Morgan Deters

2012-07-08	Bugs resolved by this commit: #314, #322, #359, #364, #365.	Morgan Deters
	See below for details. * Fix the "assert" name-collision bug (resolves bug #364). Our identifiers should never be named "assert", as that's a preprocessor definition in <assert.h>, which is often #included indirectly (so simply having a policy of not including <assert.h> isn't good enough---one of our dependences might include it). It was once the case that we didn't have anything named "assert", but "assert()" has now crept back in. Instead, name things "assertFoo()" or similar. Thanks to Tim for the report. To fix this, I've changed some of Dejan's circuit-propagator code from "assert()" to "assertTrue()". Ditto for Andy's explanation manager. Guys, if you prefer a different name in your code, please change it. * Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365). Inner lets now shadow outer lets (previously, they incorrectly gave an error). Additionally, while looking at this, I found that a sequential let was implemented rather than a parallel let. This is now fixed. Thanks to Liana for the report. * Remove ANTLR parser generation warnings in CVC parser (resolves bug #314). * There were a lot of Debug lines in bitvectors that had embedded toString() calls. This wasted a LOT of time in debug builds for BV benchmarks (like in "make regress"). Added if(Debug.isOn(...)) guards; much faster now. * Support for building public-facing interface documentation only (as opposed to all internals documentation). Now "make doc" does the public-facing and "make doc-internals" does documentation of everything. (Along with changes to the nightly build script---which will now build and publish both types of Doxygen documentation---this resolves bug #359). * Fix the lambda typechecking bug (resolves bug #322). Thanks to Andy for the report (a long long time ago--sorry). * The default output language for all streams is now based on the current set of Options (if there is one). This has been a constant annoyance, especially when stringstreams are used to construct output. However, it doesn't work for calls from outside the library, so it's mainly an annoyance-fixer for CVC4 library code itself. * Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that are used only in assertions-enabled builds (and thus give warnings in production builds). This was briefly discussed at the meeting this week.
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-02-20	portfolio merge	Morgan Deters

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

2011-09-29	Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵	Morgan Deters
	and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
2011-09-24	Fix to building and linking for unit tests. (This should fix the ↵	Morgan Deters
	segfaulting units in optimized-dynamic. The problem was that the code incorrectly determined the address of one of the thread-scoped global variables, and I think it's because the same library was linked twice into the unit test in two different ways, confusing the runtime support code.)
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-04-25	Weekend work. The main points:	Morgan Deters
	* Type::getCardinality() returns the cardinality for for all types. Theories give a cardinality in the their kinds file. For cardinalities that depend on a type argument, a "cardinality computer" function is named in the kinds file, which takes a TypeNode and returns its cardinality. * There's a bitmap for the set of "active theories" in the TheoryEngine. Theories become "active" when a term that is owned by them, or whose type is owned by them, is pre-registered (run CVC4 with --verbose to see theory activation). Non-active theories don't get any calls for check() or propagate() or anything, and if we're running in single-theory mode, the shared term manager doesn't have to get involved. This is really important for get() performance (which can only skimp on walking the entire sub-DAG only if the theory doesn't require it AND the shared term manager doesn't require it). * TheoryEngine now does not call presolve(), registerTerm(), notifyRestart(), etc., on a Theory if that theory doesn't declare that property in its kinds file. To avoid coding errors, mktheorytraits greps the theory header and gives warnings if: + the theory appears to declare one of the functions (check, propagate, etc.) that isn't listed among its kinds file properties (but probably should be) + the theory appears NOT to declare one of the functions listed in its kinds file properties * some bounded token stream work
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-27	make dist-building more pleasant (put .tar.gz in builds/ directory)	Morgan Deters

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-13	link TAGS file into builds/ directory, when built. Resolves bug #195	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-09-01	"make check" now places binaries in the proper place before doing the ↵	Morgan Deters
	checks; this closes bug 46 finally, though the major annoyances related to this bug already had been fixed long ago
2010-04-08	A handful of build system fixes:	Morgan Deters
	* (test/unit/Makefile.am) libtool was being passed relative paths of sources in .cpp, confusing lcov if -b wasn't given. Fixed. Closes bug #102. * (configure.ac) --enable-coverage now implies --enable-static --enable-static-binary --disable-shared. * (configure.ac) Create top-level config.status for informational and re-configuration purposes. * (configure.ac) Remove -fvisibility=hidden for debug builds. Closes bug #104. * (test/unit/Makefile.am) Build unit tests with -Wall. * (various unit tests) Fixed trivially-fixable warnings in building unit tests. (Signedness in comparison, unused variables, etc.) * (Makefile.builds.in) Copy the binary correctly if it is static. (It was failing, but only with --enable-static --enable-shared --enable-static-binary.) Closes bug #103. * (src/parser/Makefile.am) libcvc4parser.so now links with libcvc4.so. * Other minor cleanups to the build system.
2010-03-08	This fixes regressions at levels >= 1 which were failing	Morgan Deters
	* implement zombification and garbage collection of NodeValues (but GC not turned on yet) * implement removal of key nodes from all attribute tables * audit NodeBuilder and fix memory leaks and improper reference-count management. This is in many places a re-write. Clearly documented invariants on NodeBuilder state. (Closes Bug 38) * created a "BackedNodeBuilder" that can be used to construct NodeBuilders with a stack-based backing store for a size that's not a compile-time constant. * NodeValues no longer depend on Node for toStream()'ing * make unit test-building "silent" with --enable-silent-rules * (Makefile.am, Makefile.builds.in) fix top-level build system so that "make regressN" works with unbuilt/out-of-date source trees in the expected way. * (various) code cleanup, documentation, formatting
2010-02-22	fix bug 33 (statically link the "cvc4" binary); also main driver cleanup	Morgan Deters

2010-02-03	Addressed many of the concerns of bug 10 (build system code review).	Morgan Deters
	Some parts split into other bugs: 19, 20, 21. Addressed concerns of bug 11 (util package code review). Slight parser source file modifications: file comments, #included headers in generated parsers/lexers Added CVC4::Result propagation back through MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when verbosity is not requested.
2010-01-26	fixes to build structure, util classes, lots of fixes to Node and ↵	Morgan Deters
	NodeBuilder. outstanding SEGVs fixed
2009-12-17	coding standard fix on SmtEngine; fix recursive make	Morgan Deters

2009-12-08	work on propositional layer, expression builder support for large ↵	Morgan Deters
	expressions, output classes, and minisat
2009-12-05	more build system work	Morgan Deters